Documentation

Lean 4 Proof

def bequestHerfindahl (N : ℕ) : ℝ := 1 / ↑N

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:76

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file