Commit 2026-03-20 09:45 8093a4a3

View on Github →

chore: rename Ordinal.Principal → Ordinal.IsPrincipal (#36793) See Zulip.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

added theorem Ordinal.IsInitial.isPrincipal_add

added theorem Ordinal.IsInitial.isPrincipal_mul

added theorem Ordinal.IsInitial.isPrincipal_opow

deleted theorem Ordinal.IsInitial.principal_add

deleted theorem Ordinal.IsInitial.principal_mul

deleted theorem Ordinal.IsInitial.principal_opow

added theorem Ordinal.isPrincipal_add_omega

added theorem Ordinal.isPrincipal_add_ord

added theorem Ordinal.isPrincipal_mul_omega

added theorem Ordinal.isPrincipal_mul_ord

added theorem Ordinal.isPrincipal_opow_omega

added theorem Ordinal.isPrincipal_opow_ord

deleted theorem Ordinal.principal_add_omega

deleted theorem Ordinal.principal_add_ord

deleted theorem Ordinal.principal_mul_omega

deleted theorem Ordinal.principal_mul_ord

deleted theorem Ordinal.principal_opow_omega

deleted theorem Ordinal.principal_opow_ord

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

added theorem Ordinal.IsPrincipal.iterate_lt

added def Ordinal.IsPrincipal

deleted theorem Ordinal.Principal.iterate_lt

deleted def Ordinal.Principal

added theorem Ordinal.exists_lt_add_of_not_isPrincipal_add

deleted theorem Ordinal.exists_lt_add_of_not_principal_add

added theorem Ordinal.isPrincipal_add_iff_add_left_eq_self

added theorem Ordinal.isPrincipal_add_iff_add_lt_ne_self

added theorem Ordinal.isPrincipal_add_iff_zero_or_omega0_opow

added theorem Ordinal.isPrincipal_add_mul_of_isPrincipal_add

added theorem Ordinal.isPrincipal_add_of_isPrincipal_mul

added theorem Ordinal.isPrincipal_add_of_isPrincipal_mul_opow

added theorem Ordinal.isPrincipal_add_of_le_one

added theorem Ordinal.isPrincipal_add_omega0

added theorem Ordinal.isPrincipal_add_omega0_opow

added theorem Ordinal.isPrincipal_add_one

added theorem Ordinal.isPrincipal_add_opow_of_isPrincipal_add

added theorem Ordinal.isPrincipal_iff_of_monotone

added theorem Ordinal.isPrincipal_mul_iff_le_two_or_omega0_opow_opow

added theorem Ordinal.isPrincipal_mul_iff_mul_left_eq

added theorem Ordinal.isPrincipal_mul_of_le_two

added theorem Ordinal.isPrincipal_mul_omega0

added theorem Ordinal.isPrincipal_mul_omega0_opow_opow

added theorem Ordinal.isPrincipal_mul_one

added theorem Ordinal.isPrincipal_mul_two

added theorem Ordinal.isPrincipal_one_iff

added theorem Ordinal.isPrincipal_opow_omega0

added theorem Ordinal.isPrincipal_swap_iff

added theorem Ordinal.isPrincipal_zero

added theorem Ordinal.isSuccLimit_of_isPrincipal_add

added theorem Ordinal.isSuccLimit_of_isPrincipal_mul

deleted theorem Ordinal.isSuccLimit_of_principal_add

deleted theorem Ordinal.isSuccLimit_of_principal_mul

modified theorem Ordinal.mul_eq_opow_log_succ

added theorem Ordinal.nfp_le_of_isPrincipal

deleted theorem Ordinal.nfp_le_of_principal

deleted theorem Ordinal.not_bddAbove_principal

added theorem Ordinal.not_bddAbove_setOf_isPrincipal

added theorem Ordinal.not_isPrincipal_iff

added theorem Ordinal.not_isPrincipal_iff_of_monotone

deleted theorem Ordinal.not_principal_iff

deleted theorem Ordinal.not_principal_iff_of_monotone

added theorem Ordinal.op_eq_self_of_isPrincipal

deleted theorem Ordinal.op_eq_self_of_principal

deleted theorem Ordinal.principal_add_iff_add_left_eq_self

deleted theorem Ordinal.principal_add_iff_add_lt_ne_self

deleted theorem Ordinal.principal_add_iff_zero_or_omega0_opow

deleted theorem Ordinal.principal_add_mul_of_principal_add

deleted theorem Ordinal.principal_add_of_le_one

deleted theorem Ordinal.principal_add_of_principal_mul

deleted theorem Ordinal.principal_add_of_principal_mul_opow

deleted theorem Ordinal.principal_add_omega0

deleted theorem Ordinal.principal_add_omega0_opow

deleted theorem Ordinal.principal_add_one

deleted theorem Ordinal.principal_add_opow_of_principal_add

deleted theorem Ordinal.principal_iff_of_monotone

deleted theorem Ordinal.principal_mul_iff_le_two_or_omega0_opow_opow

deleted theorem Ordinal.principal_mul_iff_mul_left_eq

deleted theorem Ordinal.principal_mul_of_le_two

deleted theorem Ordinal.principal_mul_omega0

deleted theorem Ordinal.principal_mul_omega0_opow_opow

deleted theorem Ordinal.principal_mul_one

deleted theorem Ordinal.principal_mul_two

deleted theorem Ordinal.principal_one_iff

deleted theorem Ordinal.principal_opow_omega0

deleted theorem Ordinal.principal_swap_iff

deleted theorem Ordinal.principal_zero