mathlib documentation


Adjoining elements to form subalgebras: relation to polynomials #

In this file we prove a few results representing algebra.adjoin R s as the range of mv_polynomial.aeval or polynomial.aeval.

Tags #

adjoin, algebra, polynomials

theorem algebra.adjoin_eq_range (R : Type u) {A : Type v} (s : set A) [comm_semiring R] [comm_semiring A] [algebra R A] :
theorem algebra.adjoin_range_eq_range_aeval (R : Type u) {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] {σ : Type u_1} (f : σ → A) :
theorem algebra.adjoin_singleton_eq_range_aeval (R : Type u) {A : Type v} [comm_semiring R] [comm_semiring A] [algebra R A] (x : A) :