Documentation

Lean 4 Proof

def estateTaxRevenue (τ_E W : ℝ) : ℝ := τ_E * W

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:39

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file