Commit 2025-01-05 04:19 3c125512

View on Github →

feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Arithmetic.lean

added theorem Cardinal.add_mk_eq_self

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.mk_congr_lift

added theorem Cardinal.mk_image_embedding

added theorem Cardinal.mk_image_embedding_lift

added theorem Cardinal.mk_preimage_equiv

added theorem Cardinal.mk_preimage_equiv_lift

added theorem Cardinal.mk_range_inl

added theorem Cardinal.mk_range_inr