English
If S generates an additive monoid M, the evaluation map from MvPolynomial on S to AddMonoidAlgebra R M is surjective.
Русский
Если S порождает аддитивный моноид M, то сопоставление MvPolynomial(S,R) → R[M] сюръективно.
LaTeX
$$$\\mathrm{mvPolynomial\\_aeval}\\;\\text{surjective}$$$
Lean4
/-- If a set `S` generates, as algebra, `MonoidAlgebra R M`, then the image of the union of the
supports of elements of `S` generates `MonoidAlgebra R M`. -/
theorem support_gen_of_gen' {S : Set (MonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) :
Algebra.adjoin R (of R M '' ⋃ f ∈ S, (f.support : Set M)) = ⊤ :=
by
suffices (of R M '' ⋃ f ∈ S, (f.support : Set M)) = ⋃ f ∈ S, of R M '' (f.support : Set M)
by
rw [this]
exact support_gen_of_gen hS
simp only [Set.image_iUnion]
