starRing — Mathlib

English

StarSubalgebra carries a StarRing structure: the star operation, addition and multiplication are inherited from A via the inclusion.

Русский

StarSubalgebra обладает структурой StarRing: операция звезды, сложение и умножение наследуются от A через включение.

LaTeX

$$$\\text{StarRing}(\\text{Subtype} \\; \\{x:\\; A : x\\in S\\})$$$

Lean4

instance starRing (s : StarSubalgebra R A) : StarRing s :=
  { StarMemClass.instStar s with
    star_involutive := fun r => Subtype.ext (star_star (r : A))
    star_mul := fun r₁ r₂ => Subtype.ext (star_mul (r₁ : A) (r₂ : A))
    star_add := fun r₁ r₂ => Subtype.ext (star_add (r₁ : A) (r₂ : A)) }

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