Documentation

Lean 4 Proof

theorem curvatureK_real_eq_nat (J : ℕ) (ρ : ℝ) :
    curvatureK_real ↑J ρ = curvatureK J ρ := by
  simp only [curvatureK_real, curvatureK]

Dependency Graph

Location

thesis/CESProofs/EntryExit/Defs.lean:30

Module Section

Core definitions for the Lean formalization of Paper 1c:

In the same file