Commit 2025-05-10 21:54 c4c763b7

View on Github →

chore: add missing rfl lemmas for the tensor product of coalgebras (#23893) These are taken from https://github.com/ImperialCollegeLondon/FLT/blob/eef74b4538c8852363936dfaad23e6ffba72eca5/FLT/mathlibExperiments/Coalgebra/TensorProduct.lean simps previously generated the def lemmas, but they were badly-named, and probably not actually convenient as simp lemmas.

Estimated changes

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

Modified Mathlib/RingTheory/Coalgebra/Basic.lean

added theorem TensorProduct.comul_def

added theorem TensorProduct.comul_tmul

added theorem TensorProduct.counit_def

added theorem TensorProduct.counit_tmul

Modified Mathlib/RingTheory/Coalgebra/TensorProduct.lean

Modified Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean