Theorems · Theorem · commutative algebra

MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure

∀ {R : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : CommSemiring R] {S : Set M},
  Submonoid.closure S = ⊤ → Function.Surjective ⇑(MvPolynomial.aeval fun s => (MonoidAlgebra.of R M) ↑s)

If a set S generates a monoid M, then the image of M generates, as algebra, R[M].

Defined in

Mathlib.RingTheory.FiniteType

Cited by

0 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidCommSemiring