English
The algebra generated by all X_i contains all variables; its adjoining equals the top subalgebra.
Русский
Алгебра, порождаемая всеми X_i, содержит все переменные; её адъюнкт равен верхней подалгебре.
LaTeX
$$$\\\\operatorname{algebra.adjoin}_R (\\\\operatorname{range} (X:\\\\sigma \\\\to MvPolynomial\\\\sigma\\\\,R)) = \\\\top$$$
Lean4
@[simp]
theorem adjoin_range_X : Algebra.adjoin R (range (X : σ → MvPolynomial σ R)) = ⊤ :=
by
set S := Algebra.adjoin R (range (X : σ → MvPolynomial σ R))
refine top_unique fun p hp => ?_; clear hp
induction p using MvPolynomial.induction_on with
| C => exact S.algebraMap_mem _
| add p q hp hq => exact S.add_mem hp hq
| mul_X p i hp => exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _)
