Documentation

Lean 4 Proof

theorem lafferRevenue_zero_rate {B₀ η : ℝ} :
    lafferRevenue B₀ η 0 = 0 := by
  simp only [lafferRevenue]; ring

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:199

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file