toStarSubalgebra — Mathlib

English

Restriction to the range yields a StarAlgHom from A to f.range that is naturally equivalent to the original range.

Русский

Ограничение до образа дает StarAlgHom A → f.range, естественно эквивалентный исходному образу.

LaTeX

$$$ \\mathrm{rangeRestrict}(f) : A \\to⋆_R f.range $$$

Lean4

/-- Turn a non-unital star subalgebra containing `1` into a `StarSubalgebra`. -/
def toStarSubalgebra (S : NonUnitalStarSubalgebra R A) (h1 : 1 ∈ S) : StarSubalgebra R A
    where
  __ := S
  one_mem' := h1
  algebraMap_mem' r := (Algebra.algebraMap_eq_smul_one (R := R) (A := A) r).symm ▸ SMulMemClass.smul_mem r h1

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