English
The star-subalgebra generated by a set s equals the star-closure of the ordinary subalgebra generated by s: adjoin R s = (Algebra.adjoin R s).starClosure.
Русский
Звёздная подалгебра, порождаемая множеством s, совпадает со звёздным замыканием обычной подалгебры, порождаемой s: adjoin R s = (Algebra.adjoin R s).starClosure.
LaTeX
$$$\operatorname{adjoin}_{\text{StarAlg}}(R,s) = (\mathrm{Algebra.adjoin}(R,s)).\mathrm{starClosure}$$$
Lean4
/-- The minimal star subalgebra that contains `s`. -/
def adjoin (s : Set A) : StarSubalgebra R A :=
{ Algebra.adjoin R (s ∪ star s) with
star_mem' := fun hx => by
rwa [Subalgebra.mem_carrier, ← Subalgebra.mem_star_iff, Subalgebra.star_adjoin_comm, Set.union_star, star_star,
Set.union_comm] }
