Commit 2023-01-12 12:15 91043fd8

View on Github →

feat: forward port leanprover-community/mathlib#18121 (#1497)

Estimated changes

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

modified theorem FreeMonoid.lift_apply

modified theorem FreeMonoid.lift_comp_of

modified theorem FreeMonoid.lift_eval_of

added def FreeMonoid.prodAux

added theorem FreeMonoid.prodAux_eq