Commit 2022-06-05 01:29 157013da
View on Github →feat(set_theory/cardinal/cofinality): weaker definition for regular cardinals (#14433)
We weaken c.ord.cof = c to c ≤ c.ord.cof in the definition of regular cardinals, in order to slightly simplify proofs. The lemma is_regular.cof_eq shows that this leads to an equivalent definition.