Commit 2026-10-28 15:03 4ec03747

View on Github →

refactor: FreeMonoid as a one-field structure (#45212) Implement the second point in https://github.com/leanprover-community/mathlib4/pull/36934#discussion_r4345214702:

structure FreeMonoid (α : Type*) where
  /-- Convert a `List α` to a `FreeMonoid α`. -/
  ofList ::
  /-- The underlying list -/
  toList : List α

mulRecOn and the two following lemmas about it were filled in by GPT-6.1 Sol. Their names, as well as the current mulCasesOn, were changed because now that FreeMonoid is a structure, FreeMonoid.rec(On) and FreeMonoid.casesOn are auto-generated. Declarations about FreeMonoid.length/mem/reverse are all deprecated. Use list membership and List.reverse on toList-converted FreeMonoid objects and the StarMul instance in Mathlib.Algebra.Star.Free instead. New declarations are FreeMonoid.toListEquiv and Cardinal.mk_freeMonoid_eq_mk_list.

Estimated changes

added structure FreeAddMonoid
deleted def FreeMonoid.casesOn
deleted theorem FreeMonoid.casesOn_of_mul
deleted theorem FreeMonoid.casesOn_one
modified theorem FreeMonoid.length_eq_one
modified theorem FreeMonoid.length_eq_three
modified theorem FreeMonoid.length_eq_two
modified theorem FreeMonoid.length_eq_zero
modified theorem FreeMonoid.mem_mul
deleted def FreeMonoid.ofList
modified theorem FreeMonoid.ofList_flatten
deleted theorem FreeMonoid.ofList_symm
modified theorem FreeMonoid.of_injective
modified theorem FreeMonoid.of_ne_one
deleted def FreeMonoid.recOn
deleted theorem FreeMonoid.recOn_of_mul
deleted theorem FreeMonoid.recOn_one
modified def FreeMonoid.reverse
modified theorem FreeMonoid.reverse_mul
deleted def FreeMonoid.toList
deleted theorem FreeMonoid.toList_symm
added theorem FreeMonoid.«exists»
added theorem FreeMonoid.«forall»
added structure FreeMonoid
deleted def FreeMonoid
modified theorem FreeMonoid.count_apply
modified def FreeMonoid.symbols
modified theorem Traversable.toList_spec
modified theorem Cardinal.mk_freeMonoid