Theorem Cardinal.mk_range_inr

Modification history

2025-01-05 04:19

Mathlib/SetTheory/Cardinal/Basic.lean

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

Added Cardinal.mk_range_inr View on Github →