mathlib

83c1cd8a - feat(set_theory/cardinal/cofinality): `ω` is a strong limit cardinal (#14436)