Theorems · Definition · ring theory

IsGroupLikeElem.casesOn

{R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] →
          [inst_3 : Coalgebra R A] →
            {a : A} →
              {motive : IsGroupLikeElem R a → Sort u} →
                (t : IsGroupLikeElem R a) →
                  ((counit_eq_one : CoalgebraStruct.counit a = 1) →
                      (comul_eq_tmul_self : CoalgebraStruct.comul a = a ⊗ₜ[R] a) → motive ⋯) →
                    motive t

Defined in

Mathlib.RingTheory.Coalgebra.GroupLike

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCoalgebra