Commit 2026-03-26 19:34 a0705706

View on Github →

chore: golf results on principal ordinals (#36897)

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Principal.lean

added theorem Ordinal.isPrincipal_add_iff_add_self_lt

modified theorem Ordinal.isPrincipal_add_one

modified theorem Ordinal.isPrincipal_mul_one

modified theorem Ordinal.isPrincipal_one_iff