toNonUnitalStarSubalgebra — Mathlib

English

A nonunital subalgebra that is closed under star gives a nonunital star-subalgebra.

Русский

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

LaTeX

$$toNonUnitalStarSubalgebra(h_star) : NonUnitalStarSubalgebra R A$$

Lean4

/-- A non-unital subalgebra closed under `star` is a non-unital star subalgebra. -/
def toNonUnitalStarSubalgebra (h_star : ∀ x, x ∈ s → star x ∈ s) : NonUnitalStarSubalgebra R A :=
  { s with star_mem' := @h_star }

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