Documentation

Lean 4 Proof

theorem lafferRevenue_zero_at_upper {B₀ η : ℝ} (hη : η ≠ 0) :
    lafferRevenue B₀ η (1 / η) = 0 := by
  simp only [lafferRevenue]
  rw [show η * (1 / η) = 1 from mul_one_div_cancel hη]
  ring

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:204

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file