Documentation

Lean 4 Proof

theorem curvatureKReal_eq_nat (J : ℕ) (ρ : ℝ) :
    curvatureKReal ↑J ρ = curvatureK J ρ := by
  simp only [curvatureKReal, 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