Commit 2023-01-10 15:48 6420fef1

View on Github →

feat port:Algebra.FreeMonoid.Basic (#1443)

  • Dot notation not working for toList so replaced with "normal" notation

Estimated changes

added theorem FreeMonoid.casesOn_one
added theorem FreeMonoid.comp_lift
added theorem FreeMonoid.hom_eq
added def FreeMonoid.lift
added theorem FreeMonoid.lift_apply
added def FreeMonoid.map
added theorem FreeMonoid.map_comp
added theorem FreeMonoid.map_id
added theorem FreeMonoid.map_of
added def FreeMonoid.of
added theorem FreeMonoid.ofList_cons
added theorem FreeMonoid.ofList_join
added theorem FreeMonoid.ofList_map
added theorem FreeMonoid.ofList_nil
added theorem FreeMonoid.ofList_smul
added theorem FreeMonoid.ofList_symm
added theorem FreeMonoid.of_smul
added theorem FreeMonoid.recOn_one
added theorem FreeMonoid.smul_def
added theorem FreeMonoid.toList_map
added theorem FreeMonoid.toList_mul
added theorem FreeMonoid.toList_of
added theorem FreeMonoid.toList_one
added theorem FreeMonoid.toList_prod
added theorem FreeMonoid.toList_symm
added def FreeMonoid