Theorems · Definition · commutative algebra

Polynomial.toSubring

{R : Type u_1} → [inst : Ring R] → (p : Polynomial R) → (T : Subring R) → ↑p.coeffs ⊆ ↑T → Polynomial ↥T

Given a polynomial p and a subring T that contains the coefficients of p, return the corresponding polynomial whose coefficients are in T.

Defined in

Mathlib.RingTheory.Polynomial.Subring

Cited by

15 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Ring