Documentation

Lean 4 Proof

theorem taxRevenue_scale {τ_L τ_K τ_C τ_corp wL rK C Prof : ℝ} (c : ℝ) :
    taxRevenue (c * τ_L) (c * τ_K) (c * τ_C) (c * τ_corp) wL rK C Prof =
    c * taxRevenue τ_L τ_K τ_C τ_corp wL rK C Prof := by
  simp only [taxRevenue]; ring

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:109

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file