Commit 2024-08-06 05:13 50ebd3bd

View on Github →

feat(RingTheory/Coalgebra/*): add basics about sweedler notation (#12109) Though the name is called sweedler notation, no new notations are actually introduced. This PR is actually about expanding tensor product.

Estimated changes

Modified Mathlib/RingTheory/Coalgebra/Basic.lean

added def Coalgebra.Repr.arbitrary

added structure Coalgebra.Repr

added theorem Coalgebra.sum_counit_tmul_eq

added theorem Coalgebra.sum_tmul_counit_eq

Modified Mathlib/RingTheory/Coalgebra/Hom.lean

added def Coalgebra.Repr.induced

added theorem Coalgebra.sum_tmul_apply_counit_eq

added theorem Coalgebra.sum_tmul_counit_apply_eq

Modified Mathlib/RingTheory/HopfAlgebra.lean

added theorem HopfAlgebra.sum_antipode_mul_eq

added theorem HopfAlgebra.sum_antipode_mul_eq_smul

added theorem HopfAlgebra.sum_mul_antipode_eq

added theorem HopfAlgebra.sum_mul_antipode_eq_smul