Theorems · Theorem · ring theory

LinearMap.id_mul_antipode

∀ {R : Type u_1} {C : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring C] [inst_2 : HopfAlgebra R C],
  WithConv.toConv LinearMap.id * WithConv.toConv (HopfAlgebraStruct.antipode R) = 1

Defined in

Mathlib.RingTheory.HopfAlgebra.Convolution

Cited by

1 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringSemiringHopfAlgebra