Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-13 06:00 fc2e3b00

View on Github →

refactor(algebra/free_monoid): add to_list/of_list (#16926)

  • add free_monoid.to_list and free_monoid.of_list;
  • update API to explicitly use these functions;
  • fix control.fold.

Estimated changes

modified theorem free_monoid.lift_apply
modified theorem free_monoid.lift_comp_of
deleted theorem free_monoid.mul_def
modified def free_monoid.of
deleted theorem free_monoid.of_def
modified theorem free_monoid.of_injective
deleted theorem free_monoid.one_def
deleted theorem free_monoid.prod_eq_join
added theorem free_monoid.rec_on_one
added theorem free_monoid.smul_def
added theorem free_monoid.to_list_of
modified theorem traversable.fold_map_hom
deleted def traversable.free.mk