Documentation

Lean 4 Proof

theorem curvatureKReal_one (ρ : ℝ) :
    curvatureKReal 1 ρ = 0 := by
  simp [curvatureKReal]

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/CurvatureInJ.lean:63

Module Section

Paper 1c, Section 2: K(J) as the Network Engine

In the same file