Commit 2025-08-13 21:32 0019dc23

View on Github →

feat: counit (antipode a) = counit a (#25267) and unsimp sum_antipode_mul_eq_algebraMap_counit/sum_mul_antipode_eq_algebraMap_counit since they are annoying lemmas to fight against. From Toric

Estimated changes

Modified Mathlib/RingTheory/Coalgebra/Basic.lean

added theorem Coalgebra.lift_lsmul_comp_counit_comp_comul

added theorem Coalgebra.sum_counit_smul

Modified Mathlib/RingTheory/HopfAlgebra/Basic.lean

added theorem HopfAlgebra.counit_antipode

added theorem HopfAlgebra.counit_comp_antipode

deleted theorem HopfAlgebra.sum_antipode_mul_eq

added theorem HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit

modified theorem HopfAlgebra.sum_antipode_mul_eq_smul

deleted theorem HopfAlgebra.sum_mul_antipode_eq

added theorem HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit

modified theorem HopfAlgebra.sum_mul_antipode_eq_smul

Modified Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean