Documentation

Lean 4 Proof

theorem output_decomposition {Y Jσ : ℝ} (hJσ : Jσ ≠ 0) :
    Y - corporateProfit Y Jσ = Y * (1 - 1 / Jσ) := by
  simp only [corporateProfit]; field_simp

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:185

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file