Theorem Cardinal.mk_freeMonoid_eq_mk_list

Modification history

2026-10-28 15:03
Mathlib/SetTheory/Cardinal/Free.lean
refactor: `FreeMonoid` as a one-field structure (#45212) …
Added Cardinal.mk_freeMonoid_eq_mk_listView on Github →