Documentation

Lean 4 Proof

theorem taxRevenue_additive {τ_L τ_K τ_C τ_corp wL rK C Prof : ℝ} :
    taxRevenue τ_L τ_K τ_C τ_corp wL rK C Prof =
    τ_L * wL + τ_K * rK + τ_C * C + τ_corp * Prof := by
  simp only [taxRevenue]

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:116

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file