Theorem Ordinal.CNF.rec_zero

Modification history

2025-08-18 23:36

Mathlib/SetTheory/Ordinal/CantorNormalForm.lean

chore(SetTheory/Ordinal/CantorNormalForm): namespace results on the CNF (#28584)

Added Ordinal.CNF.rec_zero View on Github →