Theorem CategoryTheory.FreeMonoidalCategory.unit_eq_unit

Modification history

2023-11-29 06:54
Mathlib/CategoryTheory/Monoidal/Free/Basic.lean
fix: lean4-ify names of inductive constructors (#8652) …
Modified CategoryTheory.FreeMonoidalCategory.unit_eq_unitView on Github →
2023-05-03 13:39
Mathlib/CategoryTheory/Monoidal/Free/Basic.lean
feat: port CategoryTheory.Monoidal.Free.Basic (#2808)
Added CategoryTheory.FreeMonoidalCategory.unit_eq_unitView on Github →