Theorem Ordinal.CNF.rec_pos

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_pos View on Github →