Documentation

Lean 4 Proof

def recipientTaxRevenue (τ_R W : ℝ) (N : ℕ) : ℝ :=
  ↑N * (τ_R * perHeirWealth W N)

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:48

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file