Commit 2024-07-05 19:32 40b32a68

View on Github →

feat(CategoryTheory/Monoidal): convolution monoid (#13313) I'll use this shortly to prove basic properties of hopf monoids.

depends on: #13316

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Conv.lean

added theorem CategoryTheory.Conv.mul_eq

added theorem CategoryTheory.Conv.one_eq

added def CategoryTheory.Conv