Commit 2023-04-10 13:16 5558d43c

View on Github →

chore: update SHA for mathlib#18268, #18771, RelIso/Basic (#3362)

  • algebra.group.ulift: this is a change that was already backported in leanprover-community/mathlib#18268 to match mathlib4, only the SHA needs to be updated.
  • set_theory.cardinal.basic: the changes from leanprover-community/mathlib#18771 were already forward-ported in #3343, but the sha was not updated. Here I've also inlined all bys and generally tidied up the formatting.
  • order.rel_iso.basic (leanprover-community/mathlib#18699, leanprover-community/mathlib#18758) is now fully forward-ported too.

Estimated changes

modified def Quotient.mkRelHom
modified theorem RelIso.rel_symm_apply
modified theorem RelIso.symm_apply_rel
modified theorem acc_liftOn₂'_iff
modified theorem acc_lift₂_iff
modified theorem wellFounded_liftOn₂'_iff
modified theorem wellFounded_lift₂_iff
modified theorem Cardinal.IsLimit.aleph0_le
modified theorem Cardinal.aleph0_le_mul_iff'
modified theorem Cardinal.aleph0_le_mul_iff
modified theorem Cardinal.cantor'
modified theorem Cardinal.cantor
modified theorem Cardinal.card_le_of
modified theorem Cardinal.le_powerlt
modified theorem Cardinal.lift_infᵢ
modified theorem Cardinal.lift_infₛ
modified theorem Cardinal.lift_supₛ
modified theorem Cardinal.mk_eq_two_iff'
modified theorem Cardinal.mk_eq_two_iff
modified theorem Cardinal.mk_unionₛ_le
modified theorem Cardinal.mul_lt_aleph0_iff
modified theorem Cardinal.powerlt_le
modified theorem Cardinal.prod_eq_zero
modified theorem Cardinal.self_le_power
modified theorem Cardinal.sum_le_supᵢ
modified theorem Cardinal.three_le
modified theorem Cardinal.toNat_cast
modified theorem Cardinal.toNat_lift
modified theorem Cardinal.toNat_mul
modified theorem Cardinal.zero_powerlt