Commit 2023-05-03 13:39 8ab10391

View on Github →

feat: port CategoryTheory.Monoidal.Free.Basic (#2808)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

added inductive CategoryTheory.FreeMonoidalCategory.Hom

added inductive CategoryTheory.FreeMonoidalCategory.HomEquiv

added theorem CategoryTheory.FreeMonoidalCategory.mk_comp

added theorem CategoryTheory.FreeMonoidalCategory.mk_id

added theorem CategoryTheory.FreeMonoidalCategory.mk_l_hom

added theorem CategoryTheory.FreeMonoidalCategory.mk_l_inv

added theorem CategoryTheory.FreeMonoidalCategory.mk_tensor

added theorem CategoryTheory.FreeMonoidalCategory.mk_α_hom

added theorem CategoryTheory.FreeMonoidalCategory.mk_α_inv

added theorem CategoryTheory.FreeMonoidalCategory.mk_ρ_hom

added theorem CategoryTheory.FreeMonoidalCategory.mk_ρ_inv

added def CategoryTheory.FreeMonoidalCategory.project

added def CategoryTheory.FreeMonoidalCategory.projectMap

added def CategoryTheory.FreeMonoidalCategory.projectMapAux

added def CategoryTheory.FreeMonoidalCategory.projectObj

added def CategoryTheory.FreeMonoidalCategory.setoidHom

added theorem CategoryTheory.FreeMonoidalCategory.tensor_eq_tensor

added theorem CategoryTheory.FreeMonoidalCategory.unit_eq_unit

added inductive CategoryTheory.FreeMonoidalCategory