mathlib3

157013da - feat(set_theory/cardinal/cofinality): weaker definition for regular cardinals (#14433)

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.