Documentation

Lean 4 Proof

theorem saezTopRate_specialization {a e : ℝ} (_ha : 0 < a) (_he : 0 < e) :
    saezTopRate a e = 1 / (1 + a * e) := by
  simp only [saezTopRate]

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:342

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file