mathlib
10d3d256 - chore(set_theory/cardinal): fix name & reorder universes (#10236)

Commit
4 years ago
chore(set_theory/cardinal): fix name & reorder universes (#10236) * add `cardinal.lift_injective`, `cardinal.lift_eq_zero`; * reorder universe arguments in `cardinal.lift_nat_cast` to match `cardinal.lift` and `ulift`; * rename `cardinal.nat_eq_lift_eq_iff` to `cardinal.nat_eq_lift_iff`; * add `@[simp]` to `cardinal.lift_eq_zero`, `cardinal.lift_eq_nat_iff`, and `cardinal.nat_eq_lift_iff`.
Author
Parents
Loading