instStarRing — Mathlib

English

The quaternion algebra H(R,c1,c2,c3) is equipped with a star operation making it a star ring; star is an involution and distributes over addition and multiplication.

Русский

Кватернионная алгебра оснащена операцией звезды, образуя звездную кольцевую структуру; звезда является инволюцией и распределяется по сложению и умножению.

LaTeX

$$$\star(\star a) = a, \quad \star(a+b) = \star a + \star b, \quad \star(ab) = \star b\ \star a$$$

Lean4

instance instStarRing : StarRing ℍ[R,c₁,c₂,c₃]
    where
  star_involutive x := by simp [Star.star]
  star_add a b := by ext <;> simp [add_comm]; ring
  star_mul a b := by ext <;> simp <;> ring

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