Theorems · Inductive type · ring theory
HopfAlgebraStruct
(R : Type u) → (A : Type v) → [CommSemiring R] → [Semiring A] → Type (max u v)
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
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CommSemiringSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement · cited by 13,802
- CommSemiringstatement · cited by 10,911
Cited by22
Results whose statement or proof uses this declaration.
- HopfAlgebraStruct.antipodestatement and proof · cited by 38
- Ideal.IsHopfIdealstatement · cited by 4
- Ideal.IsHopfIdeal.casesOnstatement and proof · cited by 1
- HopfAlgebra.Quotient.antipode_comp_mkₐstatement and proof · cited by 0
- HopfAlgebra.Quotient.antipode_mkstatement and proof · cited by 0
- HopfAlgebra.mk.noConfusionstatement and proof · cited by 0
- Ideal.IsHopfIdeal.antipode_memstatement and proof · cited by 0
- Ideal.IsHopfIdeal.recOnstatement and proof · cited by 0
- HopfAlgebraStruct.mk.noConfusionstatement · cited by 0
- HopfAlgebra.casesOnstatement and proof · cited by 0
- HopfAlgebra.noConfusionproof · cited by 0
- HopfAlgebra.noConfusionTypeproof · cited by 0