range — Mathlib

English

Range of a NonUnitalAlgHom φ forms a NonUnitalStarSubalgebra of B.

Русский

Образ отображения NonUnitalAlgHom φ образует неединичную звёздную подпалгебру B.

LaTeX

$$NonUnitalStarAlgHom.range(φ) is a NonUnitalStarSubalgebra R B.$$

Lean4

/-- Range of an `NonUnitalAlgHom` as a `NonUnitalStarSubalgebra`. -/
protected def range (φ : F) : NonUnitalStarSubalgebra R B
    where
  toNonUnitalSubalgebra := NonUnitalAlgHom.range (φ : A →ₙₐ[R] B)
  star_mem' := by rintro _ ⟨a, rfl⟩; exact ⟨star a, map_star φ a⟩

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