algebra

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.algebra

English

If S is a commutative semiring and R an S-algebra, then ℍ(R) carries an Algebra S-structure.

Русский

Если S — коммутативное полугруппа, а R — алгебра над S, то ℍ(R) имеет структуру Algebra S-над S.

LaTeX

$$$$ \mathbb{H}(R) \text{ is an algebra over } S.$$$$

Lean4

protected instance algebra [CommSemiring S] [Algebra S R] : Algebra S ℍ[R] :=
  inferInstanceAs <| Algebra S ℍ[R,-1,0,-1]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru