structure Def1521.IsLeftIntegral (k : Type u) [CommRing k] (H : Type v) [Ring H] [Algebra k H] [Coalgebra k H] (I : H) : Prop

A left integral in H is an element I such that x * I = ε(x) • I for every x ∈ H, where ε is the counit (Definition 1.52.1).

• integral_prop (x : H) : x * I = CoalgebraStruct.counit x • I

structure Def1521.IsRightIntegral (k : Type u) [CommRing k] (H : Type v) [Ring H] [Algebra k H] [Coalgebra k H] (I : H) : Prop

A right integral in H is an element I such that I * x = ε(x) • I for every x ∈ H (Definition 1.52.1).

• integral_prop (x : H) : I * x = CoalgebraStruct.counit x • I

def Def1521.Def_1_52_1_IsLeftIntegral (k : Type u_1) [CommRing k] (H : Type u_2) [Ring H] [Algebra k H] [Coalgebra k H] (I : H) : Prop

Named alias for Definition 1.52.1 (left integrals in an algebra with counit).

def Def1521.Def_1_52_1_IsRightIntegral (k : Type u_1) [CommRing k] (H : Type u_2) [Ring H] [Algebra k H] [Coalgebra k H] (I : H) : Prop

Named alias for Definition 1.52.1 (right integrals in an algebra with counit).