English
The set underlying the star-algebra generated by restrict_s(id) equals the union of the span of 1 and the adjoin of restrict_s(id).
Русский
Множество, лежащее в основании звёздной подалгебры, порожденной ограничением id, равно объединению спроста́ единицы и порожденной подалгебры restrict_s(id).
LaTeX
$$$\operatorname{StarAlgebra.adjoin}_{\mathbb{K}}\{\mathrm{restrict}_{s}(\mathrm{id}_{\mathbb{K}})\} = \operatorname{span}_{\mathbb{K}}\{1\} \cup \operatorname{adjoin}_{\mathbb{K}}\{\mathrm{restrict}_{s}(\mathrm{id}_{\mathbb{K}})\}.$$$
Lean4
theorem adjoin_id_eq_span_one_union (s : Set 𝕜) :
((StarAlgebra.adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))}) : Set C(s, 𝕜)) =
span 𝕜 ({(1 : C(s, 𝕜))} ∪ (adjoin 𝕜 {(restrict s (.id 𝕜) : C(s, 𝕜))})) :=
by
ext x
rw [SetLike.mem_coe, SetLike.mem_coe, ← StarAlgebra.adjoin_nonUnitalStarSubalgebra, ← StarSubalgebra.mem_toSubalgebra,
← Subalgebra.mem_toSubmodule, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_union, span_eq_toSubmodule]
