Documentation

Lean 4 Proof

theorem revenue_equivalence {τ W : ℝ} {N : ℕ} (hN : 0 < N) :
    recipientTaxRevenue τ W N = estateTaxRevenue τ W := by
  simp only [recipientTaxRevenue, estateTaxRevenue, perHeirWealth]
  have hNne : (↑N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  field_simp

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:102

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file