mathlib3
c89d3194 - feat(set_theory/cardinal): add `cardinal.aleph_0_le_mul_iff'` (#14648)

Commit

3 years ago

feat(set_theory/cardinal): add `cardinal.aleph_0_le_mul_iff'` (#14648) This version provides a more useful `iff.mpr`. Also review 2 proofs.

Author

urkud

Parents