Documentation

Lean 4 Proof

theorem perCapitaSurplus_eq_K_div_J {J ρ : ℝ} (_hJ : J ≠ 0) :
    perCapitaSurplus J ρ = curvatureKReal J ρ / J := by
  simp only [perCapitaSurplus, curvatureKReal]
  have hJ2 : J ^ 2 = J * J := sq J
  rw [hJ2, div_div]

Dependency Graph

Location

thesis/CESProofs/EntryExit/Calculus.lean:303

Module Section

Paper 1c: Formal Calculus on K(J) and V(J)

In the same file