Theorems · Theorem · ring theory

HopfAlgebra.mul_antipode_rTensor_comul

∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} [self : HopfAlgebra R A],
  LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul =
    Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit

One of the antipode axioms for a Hopf algebra.

Defined in: Mathlib.RingTheory.HopfAlgebra.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 60 from the axioms · uses propext, Quot.sound
Assumes: HopfAlgebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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

RingHom.idstatement · cited by 18,349
Semiringstatement and proof · cited by 13,802
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement · cited by 10,215
TensorProductstatement · cited by 2,545
LinearMap.compstatement · cited by 1,642
LinearMap.rTensorstatement · cited by 266
Algebra.linearMapstatement · cited by 157
CoalgebraStruct.comulstatement · cited by 118
CoalgebraStruct.counitstatement · cited by 108
HopfAlgebrastatement and proof · cited by 59
LinearMap.mul'statement · cited by 47

Cited by2

Results whose statement or proof uses this declaration.

HopfAlgebra.sum_antipode_mul_eq_algebraMap_counitproof · cited by 3
HopfAlgebra.mul_antipode_rTensor_comul_applyproof · cited by 2