star_self_mem — Mathlib

English

Under suitable topological hypotheses, the elemental subalgebra generated by a normal element carries a commutative ring structure.

Русский

При соответствующих топологических гипотезах подалгебра, порожденная нормальным элементом, имеет коммутативную кольцевую структуру.

LaTeX

$$instance (R,A) [T2Space A] {x:A} [IsStarNormal x] : CommRing (elemental R x)$$

Lean4

@[simp, aesop safe (rule_sets := [SetLike])]
theorem star_self_mem (x : A) : star x ∈ elemental R x :=
  star_mem <| self_mem R x

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