Documentation

Lean 4 Proof

theorem perCapitaSurplus_alt {J : ℝ} (hJ : J ≠ 0) (ρ : ℝ) :
    perCapitaSurplus J ρ = (1 - ρ) * (J⁻¹ - (J ^ 2)⁻¹) := by
  simp only [perCapitaSurplus]
  field_simp

Dependency Graph

Location

thesis/CESProofs/EntryExit/Calculus.lean:167

Module Section

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

In the same file