instHopfAlgebra — Mathlib

English

Laurent polynomials A[T; T^{-1}] inherit a Hopf algebra structure from the underlying AddMonoidAlgebra on Z.

Русский

Лоурентовы многочлены A[T; T^{-1}] наследуют структуру HopfAlgebra от AddMonoidAlgebra на Z.

LaTeX

$$$\text{LaurentPolynomial.instHopfAlgebra} \;:\; \text{HopfAlgebra } R\,A[T;T^{-1}].$$$

Lean4

instance instHopfAlgebra : HopfAlgebra R A[T;T⁻¹] :=
  inferInstanceAs (HopfAlgebra R <| AddMonoidAlgebra A ℤ)

Похожие утверждения