Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-03-03 13:01
f7a6fe9e
View on Github →
feat(set_theory/cofinality): Prove simple theorems on regular cardinals (
#12328
)
Estimated changes
Modified
src/set_theory/cofinality.lean
added
theorem
cardinal.aleph'_succ_is_regular
added
theorem
cardinal.aleph_succ_is_regular
added
theorem
cardinal.is_regular.cof_eq
added
theorem
cardinal.is_regular.omega_le