# Documentation

Mathlib.RingTheory.MvPolynomial.Tower

# Algebra towers for multivariate polynomial #

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

This structure itself is provided elsewhere as MvPolynomial.isScalarTower

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

theorem MvPolynomial.aeval_map_algebraMap {R : Type u_1} (A : Type u_2) {B : Type u_3} {σ : Type u_4} [] [] [] [Algebra R A] [Algebra A B] [Algebra R B] [] (x : σB) (p : ) :
↑() (↑() p) = ↑() p
theorem MvPolynomial.aeval_algebraMap_apply {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [] [] [] [Algebra R A] [Algebra A B] [Algebra R B] [] (x : σA) (p : ) :
↑(MvPolynomial.aeval (↑() x)) p = ↑() (↑() p)
theorem MvPolynomial.aeval_algebraMap_eq_zero_iff {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [] [] [] [Algebra R A] [Algebra A B] [Algebra R B] [] [] [] (x : σA) (p : ) :
↑(MvPolynomial.aeval (↑() x)) p = 0 ↑() p = 0
theorem MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [] [] [] [Algebra R A] [Algebra A B] [Algebra R B] [] {x : σA} {p : } (h : Function.Injective ↑()) :
↑(MvPolynomial.aeval (↑() x)) p = 0 ↑() p = 0
@[simp]
theorem Subalgebra.mvPolynomial_aeval_coe {R : Type u_1} {A : Type u_2} {σ : Type u_4} [] [] [Algebra R A] (S : ) (x : σ{ x // x S }) (p : ) :
↑(MvPolynomial.aeval fun i => ↑(x i)) p = ↑(↑() p)