Theorem CategoryTheory.Conv.one_eq

Modification history

2025-06-04 18:15
Mathlib/CategoryTheory/Monoidal/Conv.lean
feat(CategoryTheory/Monoidal): define Mon_ by using Mon_Class (#24646) …
Modified CategoryTheory.Conv.one_eqView on Github →
2024-07-05 19:32
Mathlib/CategoryTheory/Monoidal/Conv.lean
feat(CategoryTheory/Monoidal): convolution monoid (#13313) …
Added CategoryTheory.Conv.one_eqView on Github →