Documentation

Lean 4 Proof

theorem lafferPeak_midpoint {η : ℝ} (_hη : 0 < η) :
    lafferPeak η = (1 / η) / 2 := by
  simp only [lafferPeak]; ring

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:211

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file