instNonUnitalSubringClass — Mathlib

English

There exists a NonUnitalSubringClass structure for NonUnitalStarSubalgebra inside a commutative ring context, inherited from the nonunital subsemiring structure and closed under negation.

Русский

Существует структура NonUnitalSubringClass для NonUnitalStarSubalgebra в рамках коммутативного кольца, наследующаяся от структуры nonunital-subsemiring и замкнутая относительно отрицания.

LaTeX

$$$\\text{NonUnitalSubringClass }(\\text{NonUnitalStarSubalgebra } R A) A$$$

Lean4

instance instNonUnitalSubringClass {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A]
    [Star A] : NonUnitalSubringClass (NonUnitalStarSubalgebra R A) A :=
  { NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass with
    neg_mem := fun _S {x} hx => neg_one_smul R x ▸ SMulMemClass.smul_mem _ hx }

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