mem_toNonUnitalSubring — Mathlib

English

Let S be a nonunital star-subalgebra of A. Then the carrier (underlying set) of its associated nonunital subring equals the carrier of S itself; i.e., for every x, x lies in S.toNonUnitalSubring if and only if x lies in S.

Русский

Пусть S — неполная звездная подпалгебра A. Тогда носитель (множество) соответствующего неполнуго неполного кольца совпадает с носителем самой S; то есть для любого x верно x ∈ S.toNonUnitalSubring тогда и только тогда, когда x ∈ S.

LaTeX

$$$(\uparrow S.toNonUnitalSubring : \text{Set } A) = S$$$

Lean4

@[simp]
theorem mem_toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] [Star A]
    {S : NonUnitalStarSubalgebra R A} {x} : x ∈ S.toNonUnitalSubring ↔ x ∈ S :=
  Iff.rfl

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