Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-29 07:35 7b8b8f13

View on Github →

feat(set_theory/ordinal_arithmetic): Characterize principal multiplicative ordinals (#11701) Two lemmas were renamed in the process:

mul_lt_omega → principal_mul_omega
opow_omega → principal_opow_omega Various others were moved to principal.lean.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

deleted theorem ordinal.mul_lt_omega

deleted theorem ordinal.mul_lt_omega_opow

deleted theorem ordinal.mul_omega

deleted theorem ordinal.mul_omega_dvd

added theorem ordinal.mul_two

deleted theorem ordinal.opow_lt_omega

deleted theorem ordinal.opow_omega

modified theorem ordinal.sup_opow_nat

Modified src/set_theory/ordinal_notation.lean

Modified src/set_theory/principal.lean

added theorem ordinal.mul_eq_opow_log_succ

added theorem ordinal.mul_lt_omega_opow

added theorem ordinal.mul_omega

added theorem ordinal.mul_omega_dvd

added theorem ordinal.mul_omega_opow_opow

added theorem ordinal.opow_omega

deleted theorem ordinal.opow_principal_add_is_principal_add

added theorem ordinal.opow_principal_add_of_principal_add

added theorem ordinal.principal_add_iff_zero_or_omega_opow

deleted theorem ordinal.principal_add_iff_zero_or_omega_power

added theorem ordinal.principal_add_of_principal_mul

added theorem ordinal.principal_add_of_principal_mul_opow

added theorem ordinal.principal_mul_iff_le_two_or_omega_opow_opow

added theorem ordinal.principal_mul_iff_mul_left_eq

added theorem ordinal.principal_mul_is_limit

added theorem ordinal.principal_mul_of_le_two

added theorem ordinal.principal_mul_omega

added theorem ordinal.principal_mul_omega_opow_opow

added theorem ordinal.principal_mul_one

added theorem ordinal.principal_mul_two

added theorem ordinal.principal_opow_omega