Commit 2025-06-18 18:48 a8ea88b6

View on Github →

chore: unprime the Prop-valued fields of Mon_Class (#26102) Now that we have syntax to make X explicit in them, there's really no point having the primed fields. From Toric

Estimated changes

Modified Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

Modified Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

Modified Mathlib/CategoryTheory/Monad/EquivMon.lean

Modified Mathlib/CategoryTheory/Monoidal/Bimon_.lean

deleted theorem Bimon_Class.mul_comul

deleted theorem Bimon_Class.mul_counit

deleted theorem Bimon_Class.one_comul

deleted theorem Bimon_Class.one_counit

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean

Modified Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

deleted theorem Comon_Class.comul_assoc

deleted theorem Comon_Class.comul_counit

deleted theorem Comon_Class.counit_comul

Modified Mathlib/CategoryTheory/Monoidal/Hopf_.lean

deleted theorem Hopf_Class.antipode_left

deleted theorem Hopf_Class.antipode_right

Modified Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Module.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

deleted theorem CategoryTheory.Equivalence.IsCommMon.mul_comm

deleted theorem Mon_Class.mul_assoc

deleted theorem Mon_Class.mul_one

deleted theorem Mon_Class.one_mul

Modified Mathlib/CategoryTheory/Preadditive/CommGrp_.lean