Theorem TensorProduct.counit_def

Modification history

2025-05-26 13:39
Mathlib/RingTheory/Coalgebra/Basic.lean
chore(RingTheory/HopfAlgebra): redo tensor product (#25196) …
Modified TensorProduct.counit_defView on Github →
2025-05-10 21:54
Mathlib/RingTheory/Coalgebra/Basic.lean
chore: add missing rfl lemmas for the tensor product of coalgebras (#23893) …
Added TensorProduct.counit_defView on Github →