Theorem CategoryTheory.monoidalOfHasFiniteProducts.δ_eq

Modification history

2026-07-15 16:59
Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
chore: delete deprecated declarations to the end of 2025 (#41178) …
Deleted CategoryTheory.monoidalOfHasFiniteProducts.δ_eqView on Github →
2026-05-29 13:23
Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
chore: bump toolchain to v4.31.0-rc1 (#39980)
Added CategoryTheory.monoidalOfHasFiniteProducts.δ_eqView on Github →
2026-05-17 20:27
Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
chore: remove declarations deprecated between 2021-05-15 and 2025-11-15 (#39405) …
Deleted CategoryTheory.monoidalOfHasFiniteProducts.δ_eqView on Github →
2025-11-16 17:26
Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
chore: deprecate `monoidalOfHasFiniteProducts` (#30684) …
Modified CategoryTheory.monoidalOfHasFiniteProducts.δ_eqView on Github →
2024-11-10 22:57
Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal (#17904) …
Added CategoryTheory.monoidalOfHasFiniteProducts.δ_eqView on Github →