Theorem Ordinal.isPrincipal_add_iff_add_self_lt

Modification history

2026-03-26 19:34
Mathlib/SetTheory/Ordinal/Principal.lean
chore: golf results on principal ordinals (#36897)
Added Ordinal.isPrincipal_add_iff_add_self_ltView on Github →