Mathlib Map

Structures · Algebra

HopfAlgebraStruct

Isolates the antipode of a Hopf algebra, to allow API to be constructed before proving the Hopf algebra axioms. See HopfAlgebra for documentation.

Defined in
Mathlib.RingTheory.HopfAlgebra.Basic
Shape
2 explicit arguments · adds antipode

Extends1

Extended by1

Concrete types that are instances0

No instance on a concrete type; it is reached through other classes.

How is a type an instance?

Loading the hierarchy index…

Assumed by9

Ancestors8