mathlib3 documentation

data.polynomial.monomial

Univariate monomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Preparatory lemmas for degree_basic.

@[protected, instance]
theorem polynomial.ring_hom_ext {R : Type u} [semiring R] {S : Type u_1} [semiring S] {f g : polynomial R →+* S} (h₁ : (a : R), f (polynomial.C a) = g (polynomial.C a)) (h₂ : f polynomial.X = g polynomial.X) :
f = g
@[ext]
theorem polynomial.ring_hom_ext' {R : Type u} [semiring R] {S : Type u_1} [semiring S] {f g : polynomial R →+* S} (h₁ : f.comp polynomial.C = g.comp polynomial.C) (h₂ : f polynomial.X = g polynomial.X) :
f = g