Theorem Cardinal.mul_eq_self

Modification history

2026-03-31 14:02
Mathlib/SetTheory/Cardinal/Arithmetic.lean
chore: golf `Cardinal.mul_eq_self` (#37372)
Modified Cardinal.mul_eq_selfView on Github →
2023-02-23 13:50
Mathlib/SetTheory/Cardinal/Ordinal.lean
feat: port SetTheory.Cardinal.Ordinal (#2463)
Added Cardinal.mul_eq_selfView on Github →