mathlib documentation

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

theorem is_scalar_tower.aeval_apply (R : Type u) (S : Type v) (A : Type w) [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (x : A) (p : polynomial R) :
theorem is_scalar_tower.algebra_map_aeval (R : Type u) (A : Type w) (B : Type u₁) [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra A B] [algebra R B] [is_scalar_tower R A B] (x : A) (p : polynomial R) :
theorem is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero (R : Type u) (A : Type w) (B : Type u₁) [comm_semiring R] [comm_semiring A] [comm_semiring B] [algebra R A] [algebra A B] [algebra R B] [is_scalar_tower R A B] {x : A} {p : polynomial R} (h : function.injective (algebra_map A B)) (hp : (polynomial.aeval ((algebra_map A B) x)) p = 0) :
theorem is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero_field {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [field A] [comm_semiring B] [nontrivial B] [algebra R A] [algebra R B] [algebra A B] [is_scalar_tower R A B] {x : A} {p : polynomial R} (h : (polynomial.aeval ((algebra_map A B) x)) p = 0) :
@[simp]
theorem subalgebra.aeval_coe (R : Type u) {A : Type w} [comm_semiring R] [comm_semiring A] [algebra R A] {S : subalgebra R A} {x : S} {p : polynomial R} :