Theorem Ordinal.gamma_add_one_eq_nfp

Modification history

2026-09-20 11:52
Mathlib/SetTheory/Ordinal/Veblen.lean
style: fix a few instances of 'leading by' (#43995) …
Modified Ordinal.gamma_add_one_eq_nfpView on Github →
2026-08-20 14:33
Mathlib/SetTheory/Ordinal/Veblen.lean
chore(SetTheory/Ordinal): execute deprecation TODOs (#40725) …
Added Ordinal.gamma_add_one_eq_nfpView on Github →