Documentation

Lean 4 Proof

def wealthDilutionRatio (r g : ℝ) (N : ℕ) : ℝ :=
  (1 + r) / (↑N * (1 + g))

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:68

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file