# Polynomials over subrings. #

Given a field `K`

with a subring `R`

, in this file we construct a map from polynomials in `K[X]`

with coefficients in `R`

to `R[X]`

. We provide several lemmas to deal with
coefficients, degree, and evaluation of `intPolynomial`

.
This is useful when dealing with integral elements in an extension of fields.

# Main Definitions #

`Polynomial.int`

: given a polynomial`P`

. in`K[X]`

with coefficients in a field`K`

with a subring`R`

such that all coefficients belong to`R`

,`P.int R`

is the corresponding polynomial in`R[X]`

.

def
Polynomial.int
{K : Type u_1}
[Field K]
(R : Subring K)
(P : Polynomial K)
(hP : ∀ (n : ℕ), P.coeff n ∈ R)
:

Polynomial ↥R

Given a polynomial in `K[X]`

such that all coefficients belong to the subring `R`

,
`intPolynomial`

is the corresponding polynomial in `R[X]`

.

## Equations

- Polynomial.int R P hP = { toFinsupp := { support := P.support, toFun := fun (n : ℕ) => ⟨P.coeff n, ⋯⟩, mem_support_toFun := ⋯ } }

## Instances For

@[simp]

theorem
Polynomial.int_coeff_eq
{K : Type u_1}
[Field K]
(R : Subring K)
(P : Polynomial K)
(hP : ∀ (n : ℕ), P.coeff n ∈ R)
(n : ℕ)
:

↑((Polynomial.int R P hP).coeff n) = P.coeff n

@[simp]

theorem
Polynomial.int_leadingCoeff_eq
{K : Type u_1}
[Field K]
(R : Subring K)
(P : Polynomial K)
(hP : ∀ (n : ℕ), P.coeff n ∈ R)
:

↑(Polynomial.int R P hP).leadingCoeff = P.leadingCoeff

@[simp]

theorem
Polynomial.int_monic_iff
{K : Type u_1}
[Field K]
(R : Subring K)
(P : Polynomial K)
(hP : ∀ (n : ℕ), P.coeff n ∈ R)
:

(Polynomial.int R P hP).Monic ↔ P.Monic

@[simp]

theorem
Polynomial.int_natDegree
{K : Type u_1}
[Field K]
(R : Subring K)
(P : Polynomial K)
(hP : ∀ (n : ℕ), P.coeff n ∈ R)
:

(Polynomial.int R P hP).natDegree = P.natDegree

@[simp]

theorem
Polynomial.int_eval₂_eq
{K : Type u_1}
[Field K]
(R : Subring K)
(P : Polynomial K)
(hP : ∀ (n : ℕ), P.coeff n ∈ R)
{L : Type u_2}
[Field L]
[Algebra K L]
(x : L)
:

Polynomial.eval₂ (algebraMap (↥R) L) x (Polynomial.int R P hP) = (Polynomial.aeval x) P