Theorem Cardinal.mk_equiv_of_eq

Modification history

2024-07-28 23:33

Mathlib/SetTheory/Cardinal/Ordinal.lean

chore: robustifying for debug.byAsSorry (part 13) (#15197)

Modified Cardinal.mk_equiv_of_eq View on Github →

2024-01-12 06:00

Mathlib/SetTheory/Cardinal/Ordinal.lean

feat(Cardinal): `#(α ≃ β)` and `#(α ↪ β)` in the infinite case (#9646) …

Added Cardinal.mk_equiv_of_eq View on Github →