Theorem Cardinal.mk_freeMonoid

Modification history

2026-10-28 15:03
Mathlib/SetTheory/Cardinal/Free.lean
refactor: `FreeMonoid` as a one-field structure (#45212) …
Modified Cardinal.mk_freeMonoidView on Github →
2024-10-29 15:17
Mathlib/SetTheory/Cardinal/Free.lean
feat: cardinalities of free constructions and `Nonempty (CommRing α)` (#18364) …
Added Cardinal.mk_freeMonoidView on Github →