Commit 2026-06-02 12:40 8d15a91f

View on Github →

refactor(RingTheory/Coalgebra): make the indexing type of Repr an argument (#40055) ... rather than a field. Since fields are semireducible, having a type as a field is incompatible with the new stringence of tactics to rewrite only up to defeq. For Repr, this issue shows up as soon as the indexing type isn't arbitrary anymore, usually because it is derived from one or more existing indexing types. From Toric

Estimated changes

Modified Mathlib/RingTheory/Coalgebra/Basic.lean

modified theorem Coalgebra.sum_counit_smul

modified theorem Coalgebra.sum_counit_tmul_eq

modified theorem Coalgebra.sum_tmul_counit_eq

modified theorem Coalgebra.sum_tmul_tmul_eq

Modified Mathlib/RingTheory/Coalgebra/Convolution.lean

modified theorem Coalgebra.Repr.convMul_apply

Modified Mathlib/RingTheory/Coalgebra/Hom.lean

modified def Coalgebra.Repr.induced

Modified Mathlib/RingTheory/HopfAlgebra/Basic.lean

modified theorem HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit

modified theorem HopfAlgebra.sum_antipode_mul_eq_smul

modified theorem HopfAlgebra.sum_mul_antipode_eq_algebraMap_counit

modified theorem HopfAlgebra.sum_mul_antipode_eq_smul