Theorems · Theorem · commutative algebra

MonoidAlgebra.freeAlgebra_lift_of_surjective_of_closure

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

If a set S generates an additive 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 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidCommSemiring