Theorems · Theorem · ring theory

MonoidAlgebra.ringHom_ext

∀ {R : Type u_1} {S : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] [inst_2 : Semiring S]
  {f g : MonoidAlgebra R M →+* S},
  (∀ (r : R), f (MonoidAlgebra.single 1 r) = g (MonoidAlgebra.single 1 r)) →
    (∀ (m : M), f (MonoidAlgebra.single m 1) = g (MonoidAlgebra.single m 1)) → f = g

If two ring homomorphisms from R[M] are equal on all single m 1 and single 1 r, then they are equal.

Defined in

Mathlib.Algebra.MonoidAlgebra.Defs

Cited by

7 results in Mathlib

Foundations

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

Assumes

SemiringMulOneClassSemiring