toSubalgebra — Mathlib

English

If S is a NonUnitalSubalgebra of A containing 1, then S can be regarded as a Subalgebra of A by using 1 ∈ S and the natural action of R.

Русский

Если S — неунитальное подалгебра A, содержащее 1, то его можно рассматривать как подалгебру A, используя 1 ∈ S и естественное действие R.

LaTeX

$$$(\text{toSubalgebra}(S, 1)) \text{ is a Subalgebra of } A$$$

Lean4

/-- Turn a non-unital subalgebra containing `1` into a subalgebra. -/
def toSubalgebra (S : NonUnitalSubalgebra R A) (h1 : (1 : A) ∈ S) : Subalgebra R A :=
  { S with
    one_mem' := h1
    algebraMap_mem' := fun r => (Algebra.algebraMap_eq_smul_one (R := R) (A := A) r).symm ▸ SMulMemClass.smul_mem r h1 }

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