Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-02 06:23 fefe359d

View on Github →

feat(set_theory/principal): prove theorems about additive principal ordinals (#11704)

Estimated changes

Modified src/set_theory/cardinal_ordinal.lean

added theorem cardinal.aleph_is_principal_add

added theorem cardinal.ord_is_principal_add

Modified src/set_theory/ordinal_arithmetic.lean

deleted theorem ordinal.add_absorp

deleted theorem ordinal.add_absorp_iff

deleted theorem ordinal.add_lt_omega

deleted theorem ordinal.add_lt_omega_opow

deleted theorem ordinal.add_omega

deleted theorem ordinal.add_omega_opow

deleted theorem ordinal.mul_omega_opow_opow

Modified src/set_theory/ordinal_notation.lean

Modified src/set_theory/principal.lean

added theorem ordinal.add_absorp

added theorem ordinal.add_omega

added theorem ordinal.add_omega_opow

added theorem ordinal.mul_principal_add_is_principal_add

added theorem ordinal.opow_principal_add_is_principal_add

added theorem ordinal.principal_add_iff_add_left_eq_self

added theorem ordinal.principal_add_iff_zero_or_omega_power

added theorem ordinal.principal_add_is_limit

added theorem ordinal.principal_add_of_le_one

added theorem ordinal.principal_add_omega

added theorem ordinal.principal_add_omega_opow

added theorem ordinal.principal_add_one