Documentation

Lean 4 Proof

theorem profitToFactor_ratio {Y Jσ : ℝ} (hJσ : 1 < Jσ) (_hY : Y ≠ 0) :
    corporateProfit Y Jσ / (Y - corporateProfit Y Jσ) = 1 / (Jσ - 1) := by
  simp only [corporateProfit]
  have hJσ_ne : Jσ ≠ 0 := ne_of_gt (by linarith : 0 < Jσ)
  have _hJσm1 : Jσ - 1 ≠ 0 := ne_of_gt (by linarith)
  field_simp

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:420

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file