Documentation

Lean 4 Proof

def perHeirWealth (W : ℝ) (N : ℕ) : ℝ := W / ↑N

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:43

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file