English
The same identity as above, written with a + between span and adjoin: the adjoin of id equals the span of 1 plus the adjoin of id.
Русский
То же самое, но записано через сложение: подалгебра адъойн равна сумме спана от единицы и адъойна от id.
LaTeX
$$$\operatorname{StarAlgebra.adjoin}_{\mathbb{K}}\{\mathrm{restrict}_{s}(\mathrm{id}_{\mathbb{K}})\} = (\operatorname{span}_{\mathbb{K}}\{1\}) + (\operatorname{adjoin}_{\mathbb{K}}\{\mathrm{restrict}_{s}(\mathrm{id}_{\mathbb{K}})\}).$$$
Lean4
theorem adjoin_id_eq_span_one_add (s : Set 𝕜) :
((StarAlgebra.adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))}) : Set C(s, 𝕜)) =
(span 𝕜 {(1 : C(s, 𝕜))} : Set C(s, 𝕜)) + (adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))}) :=
by
ext x
rw [SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra, ← StarSubalgebra.mem_toSubalgebra, ←
Subalgebra.mem_toSubmodule, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, mem_sup]
simp [Set.mem_add]
