# Algebra towers for polynomial #

This file proves some basic results about the algebra tower structure for the type R[X].

This structure itself is provided elsewhere as Polynomial.isScalarTower

When you update this file, you can also try to make a corresponding update in RingTheory.MvPolynomial.Tower.

@[simp]
theorem Polynomial.aeval_map_algebraMap {R : Type u_1} (A : Type u_2) {B : Type u_3} [] [] [] [Algebra R A] [Algebra A B] [Algebra R B] [] (x : B) (p : ) :
@[simp]
theorem Polynomial.eval_map_algebraMap {R : Type u_1} (A : Type u_2) [] [] [Algebra R A] (P : ) (a : A) :
theorem Polynomial.aeval_algebraMap_apply {R : Type u_1} {A : Type u_2} (B : Type u_3) [] [] [] [Algebra R A] [Algebra A B] [Algebra R B] [] (x : A) (p : ) :
(Polynomial.aeval ((algebraMap A B) x)) p = (algebraMap A B) ( p)
@[simp]
theorem Polynomial.aeval_algebraMap_eq_zero_iff {R : Type u_1} {A : Type u_2} (B : Type u_3) [] [] [] [Algebra R A] [Algebra A B] [Algebra R B] [] [] [] (x : A) (p : ) :
(Polynomial.aeval ((algebraMap A B) x)) p = 0 p = 0
theorem Polynomial.aeval_algebraMap_eq_zero_iff_of_injective {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [Algebra R A] [Algebra A B] [Algebra R B] [] {x : A} {p : } (h : Function.Injective (algebraMap A B)) :
(Polynomial.aeval ((algebraMap A B) x)) p = 0 p = 0
@[simp]
theorem Subalgebra.aeval_coe {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (S : ) (x : { x : A // x S }) (p : ) :
(Polynomial.aeval x) p = ( p)