Documentation

Lean 4 Proof

theorem afterTax_capital_income_eq {τ_K s_K Y : ℝ} :
    (1 - τ_K) * (s_K * Y) = (1 - τ_K) * s_K * Y := by ring

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:464

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file