Mathlib Changelog
v4
Changelog
About
Github
Theorem
Cardinal.aleph1_eq_lift
Modification history
2024-10-22 14:15
Mathlib/SetTheory/Cardinal/Aleph.lean
feat(SetTheory/Cardinal/Basic): `lift (aleph' o) = aleph' (lift o)` (#16306) …
Added
Cardinal.aleph1_eq_lift
View on Github →