Commit 2024-10-17 03:53 08804ac5

View on Github →

chore(SetTheory/Ordinal/Arithmetic): omega0_isLimit → isLimit_omega0 (#17744) I missed this rename in #17673.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

modified theorem Cardinal.exists_aleph

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Cardinal.isLimit_ord

deleted theorem Cardinal.ord_isLimit

added theorem Ordinal.isLimit_omega0

deleted theorem Ordinal.omega0_isLimit

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean