Documentation

Lean 4 Proof

theorem curvatureK_eq_curvatureKH {J : ℕ} (hJ : 0 < J) {ρ : ℝ} :
    curvatureK J ρ = curvatureKH ρ (1 / ↑J) := by
  simp only [curvatureK, curvatureKH]
  have hJr : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hJne : (J : ℝ) ≠ 0 := ne_of_gt hJr
  field_simp

Dependency Graph

Location

thesis/CESProofs/Foundations/Defs.lean:69

Module Section

Core definitions for the Lean formalization of Paper 1:

In the same file