Theorems · Theorem · ring theory

HopfAlgebra.sum_antipode_mul_eq_algebraMap_counit

∀ {R : Type u} {A : Type v} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A]
  {a : A} (repr : Coalgebra.Repr R a ι),
  ∑ i ∈ repr.index, (HopfAlgebraStruct.antipode R) (repr.left i) * repr.right i =
    (algebraMap R A) (CoalgebraStruct.counit a)

Defined in: Mathlib.RingTheory.HopfAlgebra.Basic
Cited by: 3 results in Mathlib
Foundations: Depth 61 from the axioms · uses propext, Quot.sound
Assumes: CommSemiring Semiring HopfAlgebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
RingHom.idstatement and proof · cited by 18,349
Semiringstatement and proof · cited by 13,802
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement and proof · cited by 10,215
RingHomstatement · cited by 10,189
Finset.sumstatement · cited by 5,195
Algebra.algebraMapstatement and proof · cited by 4,706
TensorProduct.tmulproof · cited by 1,182
map_sumproof · cited by 455
LinearMap.rTensorproof · cited by 266
CoalgebraStruct.counitstatement and proof · cited by 108

Cited by3

Results whose statement or proof uses this declaration.

HopfAlgebra.antipode_comp_mul_comp_commproof · cited by 1
LinearMap.antipode_mul_idproof · cited by 1
HopfAlgebra.sum_antipode_mul_eq_smulproof · cited by 0