Def CategoryTheory.Monoidal.induced

Modification history

2024-09-16 12:43

Mathlib/CategoryTheory/Monoidal/Transport.lean

refactor(Mathlib/CategoryTheory/Monoidal/Transport): remove `simps` at `transport` (#16819) …

Added CategoryTheory.Monoidal.induced View on Github →