Theorem Cardinal.add_mk_eq_self

Modification history

2025-01-05 04:19

Mathlib/SetTheory/Cardinal/Arithmetic.lean

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

Added Cardinal.add_mk_eq_self View on Github →