Theorems · Definition · ring theory

HopfAlgebra.casesOn

{R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        {motive : HopfAlgebra R A → Sort u_1} →
          (t : HopfAlgebra R A) →
            ([toHopfAlgebraStruct : HopfAlgebraStruct R A] →
                (mul_antipode_rTensor_comul :
                    LinearMap.mul' R A ∘ₗ LinearMap.rTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul =
                      Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit) →
                  (mul_antipode_lTensor_comul :
                      LinearMap.mul' R A ∘ₗ
                          LinearMap.lTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul =
                        Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit) →
                    motive
                      { toHopfAlgebraStruct := toHopfAlgebraStruct,
                        mul_antipode_rTensor_comul := mul_antipode_rTensor_comul,
                        mul_antipode_lTensor_comul := mul_antipode_lTensor_comul }) →
              motive t

Defined in

Mathlib.RingTheory.HopfAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiring