# mathlibdocumentation

ring_theory.polynomial.tower

# Algebra towers for polynomial #

This file proves some basic results about the algebra tower structure for the type polynomial R.

This structure itself is provided elsewhere as polynomial.is_scalar_tower

@[simp]
theorem polynomial.aeval_map_algebra_map {R : Type u_1} (A : Type u_2) {B : Type u_3} [semiring B] [ A] [ B] [ B] [ B] (x : B) (p : polynomial R) :
(polynomial.map A) p) = p
theorem polynomial.aeval_algebra_map_apply {R : Type u_1} {A : Type u_2} (B : Type u_3) [semiring B] [ A] [ B] [ B] [ B] (x : A) (p : polynomial R) :
(polynomial.aeval ( B) x)) p = B) ( p)
@[simp]
theorem polynomial.aeval_algebra_map_eq_zero_iff {R : Type u_1} {A : Type u_2} (B : Type u_3) [semiring B] [ A] [ B] [ B] [ B] [nontrivial B] (x : A) (p : polynomial R) :
(polynomial.aeval ( B) x)) p = 0 p = 0
theorem polynomial.aeval_algebra_map_eq_zero_iff_of_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [semiring B] [ A] [ B] [ B] [ B] {x : A} {p : polynomial R} (h : function.injective B)) :
(polynomial.aeval ( B) x)) p = 0 p = 0
@[simp]
theorem subalgebra.aeval_coe {R : Type u_1} {A : Type u_2} [ A] (S : A) (x : S) (p : polynomial R) :
p = ( p)