English
If a predicate holds for all generators in s and is preserved by algebra maps, addition, multiplication, and star, then it holds for all elements of adjoin R s.
Русский
Если для множества порождающих s верно некоторое свойство и оно стабильно при алгебраических отображениях, сложении, умножении и звезде, то оно верно и для всех элементов adjoin(R,s).
LaTeX
$$@[elab_as_elim] $\\text{adjoin\_induction}$: if P holds for generators and is closed under algebra map, addition, multiplication, and star, then P holds for all elements of adjoin(R,s).$$
Lean4
theorem adjoin_nonUnitalStarSubalgebra_eq_span (s : NonUnitalStarSubalgebra R A) :
(adjoin R (s : Set A)).toSubalgebra.toSubmodule = span R { 1 } ⊔ s.toSubmodule := by
rw [adjoin_eq_span, Submonoid.closure_eq_one_union, span_union, ← NonUnitalStarAlgebra.adjoin_eq_span,
NonUnitalStarAlgebra.adjoin_eq]
