Theorems · Theorem · commutative algebra

MvPolynomial.ringHom_ext

∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A]
  {f g : MvPolynomial σ R →+* A},
  (∀ (r : R), f (MvPolynomial.C r) = g (MvPolynomial.C r)) →
    (∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) → f = g

Defined in

Mathlib.Algebra.MvPolynomial.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiring