Polynomials

This file formalizes the relationship between polynomials and formal power series (FPS), following the treatment in the Algebraic Combinatorics book.

Main Content

The key insight is that polynomials can be viewed as FPSs with only finitely many nonzero coefficients. In Mathlib:

• PowerSeries R (notation: R⟦X⟧) is the type of formal power series
• Polynomial R (notation: R[X]) is the type of univariate polynomials
• Polynomial.toPowerSeries embeds polynomials into power series

Main Definitions

• FPS.IsPolynomial - A predicate characterizing when a power series is a polynomial (i.e., has only finitely many nonzero coefficients)
• FPS.polynomialSubalgebra - The K-subalgebra of polynomial power series (Theorem 7.5.2)
• FPS.polynomialSubring - The subring of polynomial power series (Theorem 7.5.2)
• FPS.polynomialSubmodule - The K-submodule of polynomial power series (Theorem 7.5.2)
• FPS.polyEval - Polynomial evaluation at an element of a K-algebra (Definition 7.5.6)
• Notation f⦃a⦄ for polynomial evaluation (corresponds to book notation f[a])

Main Results

• FPS.isPolynomial_iff_finite_support - A power series is a polynomial iff it has finite support
• FPS.isPolynomial_add - The sum of polynomials is a polynomial
• FPS.isPolynomial_mul - The product of polynomials is a polynomial
• FPS.isPolynomial_neg - The negation of a polynomial is a polynomial
• FPS.isPolynomial_sub - The difference of polynomials is a polynomial

Evaluation/Substitution (def.pol.subs)

The evaluation of a polynomial f at an element a of a K-algebra A is denoted polyEval f a or f⦃a⦄. This corresponds to Definition 7.5.6 (def.pol.subs) in the source: f[a] := Σ_{n ∈ ℕ} f_n · a^n

Key properties (Theorem 7.5.7, thm.pol.eval.a+b):

• (f + g)⦃a⦄ = f⦃a⦄ + g⦃a⦄ : eval_add'
• (f * g)⦃a⦄ = f⦃a⦄ * g⦃a⦄ : eval_mul'
• (c • f)⦃a⦄ = c • f⦃a⦄ : eval_smul'
• C(c)⦃a⦄ = algebraMap K A c : eval_C'
• X⦃a⦄ = a : eval_X'
• X^i⦃a⦄ = a^i : eval_X_pow'
• f⦃g⦃a⦄⦄ = (f.comp g)⦃a⦄ : eval_comp'

Special cases:

• f⦃x⦄ = f : eval_X_eq_self
• f⦃0⦄ = f₀ : eval_zero_eq_coeff_zero
• f⦃1⦄ = sum of coefficients : eval_one_eq_sum_coeffs

References

• Definition 7.5.1 (def.fps.pol) - Definition of polynomial as FPS with finite support ✓
• Theorem 7.5.2 (thm.fps.pol.ring) - K[x] is a subring of K[[x]] ✓
• Definition 7.5.3 (def.alg.ring) - Definition of (noncommutative) ring
• Definition 7.5.5 (def.alg.Kalg) - Definition of K-algebra
• Definition 7.5.6 (def.pol.subs) - Evaluation/substitution into polynomials ✓
• Theorem 7.5.7 (thm.pol.eval.a+b) - Properties of polynomial evaluation ✓

Definition of Polynomial as FPS with Finite Support

Definition 7.5.1 (def.fps.pol): An FPS a ∈ K⟦X⟧ is a polynomial if all but finitely many coefficients are zero.

def FPS.IsPolynomial {K : Type u_1} [CommRing K] (f : PowerSeries K) : Prop

A power series is a polynomial if it has finite support, i.e., only finitely many nonzero coefficients. This corresponds to Definition 7.5.1 (def.fps.pol) in the source.

Equations

• FPS.IsPolynomial f = {n : ℕ | (PowerSeries.coeff n) f ≠ 0}.Finite

theorem FPS.isPolynomial_iff_finite_support {K : Type u_1} [CommRing K] (f : PowerSeries K) : IsPolynomial f ↔ {n : ℕ | (PowerSeries.coeff n) f ≠ 0}.Finite

A power series is a polynomial iff its support (set of indices with nonzero coefficients) is finite.

theorem FPS.isPolynomial_of_polynomial {K : Type u_1} [CommRing K] (p : Polynomial K) : IsPolynomial ↑p

The image of a polynomial under toPowerSeries is a polynomial (in the FPS sense).

theorem FPS.isPolynomial_iff_exists_degree_bound {K : Type u_1} [CommRing K] (f : PowerSeries K) : IsPolynomial f ↔ ∃ (N : ℕ), ∀ n ≥ N, (PowerSeries.coeff n) f = 0

For a polynomial power series, there exists a degree bound such that all coefficients beyond this bound are zero. This is an equivalent characterization of polynomials.

theorem FPS.isPolynomial_iff_exists_polynomial {K : Type u_1} [CommRing K] (f : PowerSeries K) : IsPolynomial f ↔ ∃ (p : Polynomial K), f = ↑p

A power series is a polynomial iff it equals the coercion of some polynomial. This provides the key equivalence between IsPolynomial and Mathlib's Polynomial type.

noncomputable def FPS.toPolynomial {K : Type u_1} [CommRing K] (f : PowerSeries K) (hf : IsPolynomial f) : Polynomial K

Convert a polynomial power series to its corresponding polynomial. This requires a proof that the power series is a polynomial.

Equations

• FPS.toPolynomial f hf = (fun (N : ℕ) => (PowerSeries.trunc N) f) ⋯.choose

theorem FPS.coe_toPolynomial {K : Type u_1} [CommRing K] (f : PowerSeries K) (hf : IsPolynomial f) : ↑(toPolynomial f hf) = f

The polynomial corresponding to a polynomial power series coerces back to the original. This shows that toPolynomial is a left inverse of the coercion from polynomials.

theorem FPS.toPolynomial_coe {K : Type u_1} [CommRing K] (p : Polynomial K) : toPolynomial ↑p ⋯ = p

Converting a polynomial to a power series and back gives the original polynomial.

Polynomials Form a Subring of Power Series

Theorem 7.5.2 (thm.fps.pol.ring): The set K[x] is a subring of K[[x]].

@[simp]

theorem FPS.isPolynomial_zero {K : Type u_1} [CommRing K] : IsPolynomial 0

The zero power series is a polynomial.

@[simp]

theorem FPS.isPolynomial_one {K : Type u_1} [CommRing K] : IsPolynomial 1

The constant power series 1 is a polynomial.

theorem FPS.isPolynomial_add {K : Type u_1} [CommRing K] {f g : PowerSeries K} (hf : IsPolynomial f) (hg : IsPolynomial g) : IsPolynomial (f + g)

The sum of two polynomial power series is a polynomial. This is part of Theorem 7.5.2 (thm.fps.pol.ring).

theorem FPS.isPolynomial_neg {K : Type u_1} [CommRing K] {f : PowerSeries K} (hf : IsPolynomial f) : IsPolynomial (-f)

The negation of a polynomial power series is a polynomial. This is part of Theorem 7.5.2 (thm.fps.pol.ring).

theorem FPS.isPolynomial_sub {K : Type u_1} [CommRing K] {f g : PowerSeries K} (hf : IsPolynomial f) (hg : IsPolynomial g) : IsPolynomial (f - g)

The difference of two polynomial power series is a polynomial. This is part of Theorem 7.5.2 (thm.fps.pol.ring).

theorem FPS.isPolynomial_mul {K : Type u_1} [CommRing K] {f g : PowerSeries K} (hf : IsPolynomial f) (hg : IsPolynomial g) : IsPolynomial (f * g)

The product of two polynomial power series is a polynomial. This is the main content of Theorem 7.5.2 (thm.fps.pol.ring).

theorem FPS.isPolynomial_smul {K : Type u_1} [CommRing K] {f : PowerSeries K} (c : K) (hf : IsPolynomial f) : IsPolynomial (c • f)

Scalar multiplication of a polynomial power series is a polynomial. This is part of Theorem 7.5.2 (thm.fps.pol.ring).

K[x] as a Subalgebra of K[[x]]

Theorem 7.5.2 (thm.fps.pol.ring): The set K[x] is a subring of K[[x]] (closed under addition, subtraction, and multiplication, and contains 0 and 1) and a K-submodule of K[[x]] (closed under addition and scalar multiplication).

These two properties together mean that K[x] forms a K-subalgebra of K[[x]].

def FPS.polynomialSubalgebra {K : Type u_1} [CommRing K] : Subalgebra K (PowerSeries K)

The set of polynomial power series forms a K-subalgebra of K[[x]]. This is Theorem 7.5.2 (thm.fps.pol.ring) in the source: K[x] is a subring of K[[x]] (closed under +, -, *, contains 0 and 1) and a K-submodule (closed under + and scalar multiplication).

Equations

• FPS.polynomialSubalgebra = { carrier := {f : PowerSeries K | FPS.IsPolynomial f}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

def FPS.polynomialSubring {K : Type u_1} [CommRing K] : Subring (PowerSeries K)

The underlying subring of the polynomial subalgebra. This is the "subring" part of Theorem 7.5.2 (thm.fps.pol.ring): K[x] is closed under +, -, *, and contains 0 and 1.

Equations

• FPS.polynomialSubring = FPS.polynomialSubalgebra.toSubring

def FPS.polynomialSubmodule {K : Type u_1} [CommRing K] : Submodule K (PowerSeries K)

The underlying K-submodule of the polynomial subalgebra. This is the "K-submodule" part of Theorem 7.5.2 (thm.fps.pol.ring): K[x] is closed under + and scalar multiplication by elements of K.

Equations

• FPS.polynomialSubmodule = Subalgebra.toSubmodule FPS.polynomialSubalgebra

@[simp]

theorem FPS.mem_polynomialSubalgebra {K : Type u_1} [CommRing K] (f : PowerSeries K) : f ∈ polynomialSubalgebra ↔ IsPolynomial f

Membership in the polynomial subalgebra is equivalent to being a polynomial. This is the characterization of K[x] from Theorem 7.5.2 (thm.fps.pol.ring).

@[simp]

theorem FPS.mem_polynomialSubring {K : Type u_1} [CommRing K] (f : PowerSeries K) : f ∈ polynomialSubring ↔ IsPolynomial f

Membership in the polynomial subring is equivalent to being a polynomial. This is the "subring" characterization from Theorem 7.5.2 (thm.fps.pol.ring).

@[simp]

theorem FPS.mem_polynomialSubmodule {K : Type u_1} [CommRing K] (f : PowerSeries K) : f ∈ polynomialSubmodule ↔ IsPolynomial f

Membership in the polynomial submodule is equivalent to being a polynomial. This is the "K-submodule" characterization from Theorem 7.5.2 (thm.fps.pol.ring).

Rings (Noncommutative Rings)

Definition 7.5.3 (def.alg.ring): A ring (also known as a noncommutative ring) is defined in the same way as a commutative ring, except that the commutativity of multiplication axiom is removed.

In Mathlib, this is captured by the Ring typeclass. Note that "noncommutative ring" does not imply that the ring is not commutative; it merely means that commutativity is not required. Thus, any commutative ring is a noncommutative ring.

Examples of noncommutative rings:

• Matrix rings Matrix n n R for any ring R and n > 1
• The quaternions ℍ[R] (Mathlib: Quaternion)
• Endomorphism rings Module.End R M for any R-module M

theorem FPS.ring_add_assoc {R : Type u_2} [Ring R] (a b c : R) : a + (b + c) = a + b + c

Associativity of addition (Ring axiom): a + (b + c) = (a + b) + c for all a, b, c ∈ R.

theorem FPS.ring_add_comm {R : Type u_2} [Ring R] (a b : R) : a + b = b + a

Commutativity of addition (Ring axiom): a + b = b + a for all a, b ∈ R. Note: Addition is always commutative, even in noncommutative rings.

theorem FPS.ring_add_zero {R : Type u_2} [Ring R] (a : R) : a + 0 = a

Neutrality of zero (Ring axiom): a + 0 = a for all a ∈ R.

theorem FPS.ring_zero_add {R : Type u_2} [Ring R] (a : R) : 0 + a = a

Neutrality of zero (Ring axiom): 0 + a = a for all a ∈ R.

theorem FPS.ring_add_neg {R : Type u_2} [Ring R] (a : R) : a + -a = 0

Existence of additive inverse (Ring axiom): a + (-a) = 0 for all a ∈ R.

theorem FPS.ring_mul_assoc {R : Type u_2} [Ring R] (a b c : R) : a * (b * c) = a * b * c

Associativity of multiplication (Ring axiom): a * (b * c) = (a * b) * c for all a, b, c ∈ R.

theorem FPS.ring_left_distrib {R : Type u_2} [Ring R] (a b c : R) : a * (b + c) = a * b + a * c

Left distributivity (Ring axiom): a * (b + c) = a * b + a * c for all a, b, c ∈ R.

theorem FPS.ring_right_distrib {R : Type u_2} [Ring R] (a b c : R) : (a + b) * c = a * c + b * c

Right distributivity (Ring axiom): (a + b) * c = a * c + b * c for all a, b, c ∈ R.

theorem FPS.ring_mul_one {R : Type u_2} [Ring R] (a : R) : a * 1 = a

Neutrality of one (Ring axiom): a * 1 = a for all a ∈ R.

theorem FPS.ring_one_mul {R : Type u_2} [Ring R] (a : R) : 1 * a = a

Neutrality of one (Ring axiom): 1 * a = a for all a ∈ R.

theorem FPS.ring_mul_zero {R : Type u_2} [Ring R] (a : R) : a * 0 = 0

Annihilation (Ring property): a * 0 = 0 for all a ∈ R.

theorem FPS.ring_zero_mul {R : Type u_2} [Ring R] (a : R) : 0 * a = 0

Annihilation (Ring property): 0 * a = 0 for all a ∈ R.

Examples of Noncommutative Rings

The source lists several examples of noncommutative rings:

• Matrix rings R^{n×n} for any ring R (commutative if n ≤ 1, noncommutative if n > 1)
• The quaternions ℍ
• Endomorphism rings of abelian groups/modules

K-Algebras

Definition 7.5.5 (def.alg.Kalg): K-Algebras

The source defines a K-algebra as a set A equipped with four maps:

• ⊕ : A × A → A (addition)
• ⊖ : A × A → A (subtraction)
• ⊙ : A × A → A (multiplication)
• ⇀ : K × A → A (scalar multiplication)

and two elements 0⃗ ∈ A (zero) and 1⃗ ∈ A (one), satisfying three properties:

1. A is a (noncommutative) ring: The set A with ⊕, ⊖, ⊙, 0⃗, 1⃗ satisfies the ring axioms (same as commutative ring but without commutativity of multiplication).

2. A is a K-module: The set A with ⊕, ⊖, ⇀, 0⃗ satisfies the module axioms.

3. Compatibility property (equation 7.5.2): λ ⇀ (a ⊙ b) = (λ ⇀ a) ⊙ b = a ⊙ (λ ⇀ b) for all λ ∈ K and a, b ∈ A.

In Mathlib, this is captured by the Algebra typeclass, which requires:

• [Semiring A] (or [Ring A] for rings with subtraction)
• [Algebra K A] which provides scalar multiplication and the compatibility property

The key property λ(ab) = (λa)b = a(λb) is expressed via:

• Algebra.smul_mul_assoc: r • x * y = r • (x * y)
• Algebra.mul_smul_comm: x * r • y = r • (x * y)

Property 1: A is a Ring

A K-algebra A is automatically a ring. The ring axioms are satisfied. Note: The source allows noncommutative rings; in Mathlib, Ring A captures this. For commutative algebras, we use CommRing A.

theorem FPS.kalg_add_comm {A : Type u_2} [Ring A] (a b : A) : a + b = b + a

A K-algebra is a ring: addition is commutative. Label: def.alg.Kalg (Property 1)

theorem FPS.kalg_add_assoc {A : Type u_2} [Ring A] (a b c : A) : a + (b + c) = a + b + c

A K-algebra is a ring: addition is associative. Label: def.alg.Kalg (Property 1)

theorem FPS.kalg_add_zero {A : Type u_2} [Ring A] (a : A) : a + 0 = a

A K-algebra is a ring: zero is the additive identity. Label: def.alg.Kalg (Property 1)

theorem FPS.kalg_mul_assoc {A : Type u_2} [Ring A] (a b c : A) : a * (b * c) = a * b * c

A K-algebra is a ring: multiplication is associative. Label: def.alg.Kalg (Property 1)

theorem FPS.kalg_left_distrib {A : Type u_2} [Ring A] (a b c : A) : a * (b + c) = a * b + a * c

A K-algebra is a ring: left distributivity. Label: def.alg.Kalg (Property 1)

theorem FPS.kalg_right_distrib {A : Type u_2} [Ring A] (a b c : A) : (a + b) * c = a * c + b * c

A K-algebra is a ring: right distributivity. Label: def.alg.Kalg (Property 1)

theorem FPS.kalg_mul_one {A : Type u_2} [Ring A] (a : A) : a * 1 = a

A K-algebra is a ring: one is the multiplicative identity. Label: def.alg.Kalg (Property 1)

theorem FPS.kalg_one_mul {A : Type u_2} [Ring A] (a : A) : 1 * a = a

A K-algebra is a ring: one is the multiplicative identity (left). Label: def.alg.Kalg (Property 1)

Property 2: A is a K-Module

A K-algebra A is automatically a K-module. The module axioms are satisfied.

theorem FPS.kalg_smul_assoc {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (u v : K) (a : A) : u • v • a = (u * v) • a

A K-algebra is a K-module: scalar multiplication is associative. Label: def.alg.Kalg (Property 2)

theorem FPS.kalg_smul_add {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (u : K) (a b : A) : u • (a + b) = u • a + u • b

A K-algebra is a K-module: scalar multiplication distributes over addition (left). Label: def.alg.Kalg (Property 2)

theorem FPS.kalg_add_smul {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (u v : K) (a : A) : (u + v) • a = u • a + v • a

A K-algebra is a K-module: scalar multiplication distributes over addition (right). Label: def.alg.Kalg (Property 2)

theorem FPS.kalg_one_smul {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (a : A) : 1 • a = a

A K-algebra is a K-module: 1 acts as identity. Label: def.alg.Kalg (Property 2)

theorem FPS.kalg_zero_smul {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (a : A) : 0 • a = 0

A K-algebra is a K-module: 0 annihilates. Label: def.alg.Kalg (Property 2)

theorem FPS.kalg_smul_zero {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (u : K) : u • 0 = 0

A K-algebra is a K-module: scalar multiplication by zero element gives zero. Label: def.alg.Kalg (Property 2)

Property 3: Compatibility (Equation 7.5.2)

The key compatibility property: λ(ab) = (λa)b = a(λb) for all λ ∈ K and a, b ∈ A.

This says that scaling a product in A by a scalar λ ∈ K is equivalent to scaling either of its two factors by λ.

theorem FPS.kalg_smul_mul_assoc {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (c : K) (a b : A) : c • (a * b) = c • a * b

The compatibility property for K-algebras: λ(ab) = (λa)b. This is equation (7.5.2) in the source. Label: def.alg.Kalg (Property 3)

theorem FPS.kalg_mul_smul_comm {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (c : K) (a b : A) : c • (a * b) = a * c • b

The compatibility property for K-algebras: λ(ab) = a(λb). This is equation (7.5.2) in the source. Label: def.alg.Kalg (Property 3)

theorem FPS.kalg_smul_mul_eq_mul_smul {K : Type u_1} [CommRing K] {A : Type u_2} [Ring A] [Algebra K A] (c : K) (a b : A) : c • a * b = a * c • b

Combined compatibility: (λa)b = a(λb). Follows from the two parts of equation (7.5.2). Label: def.alg.Kalg (Property 3)

Examples of K-Algebras

The source lists several examples of K-algebras:

• The ring K itself
• The ring K⟦X⟧ of formal power series
• The polynomial ring K[X] (as a subring of K⟦X⟧)
• The matrix ring K^{n×n} for each n ∈ ℕ
• Any quotient ring K/I where I is an ideal
• Any commutative ring containing K as a subring

The algebraMap

In Mathlib, a K-algebra A comes with a ring homomorphism algebraMap K A : K →+* A that embeds K into the center of A. This allows us to view elements of K as elements of A.

theorem FPS.algebraMap_zero {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] : (algebraMap K A) 0 = 0

algebraMap preserves zero.

theorem FPS.algebraMap_one {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] : (algebraMap K A) 1 = 1

algebraMap preserves one.

theorem FPS.algebraMap_add {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (a b : K) : (algebraMap K A) (a + b) = (algebraMap K A) a + (algebraMap K A) b

algebraMap preserves addition.

theorem FPS.algebraMap_mul {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (a b : K) : (algebraMap K A) (a * b) = (algebraMap K A) a * (algebraMap K A) b

algebraMap preserves multiplication.

theorem FPS.algebraMap_commutes {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (r : K) (x : A) : (algebraMap K A) r * x = x * (algebraMap K A) r

Elements in the image of algebraMap commute with all elements of A. This is a key property: algebraMap K A lands in the center of A.

theorem FPS.smul_eq_algebraMap_mul {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (r : K) (x : A) : r • x = (algebraMap K A) r * x

Scalar multiplication is related to algebraMap: r • x = algebraMap K A r * x.

Evaluation of Polynomials

Definition 7.5.6 (def.pol.subs): For a polynomial f ∈ K[x] and an element a of a K-algebra A, we define f[a] := Σ_{n ∈ ℕ} f_n * a^n.

In Mathlib, this is Polynomial.aeval a f for evaluation in a K-algebra A.

Implementation Notes

The book uses notation f[a] for polynomial evaluation. In Mathlib:

• Polynomial.aeval a f evaluates polynomial f at element a of a K-algebra
• Polynomial.eval₂ φ a f is more general, using a ring homomorphism φ
• Polynomial.eval a f evaluates in the base ring K itself

We provide polyEval as a wrapper matching the book's presentation.

@[reducible, inline]

abbrev FPS.polyEval {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) (a : A) : A

Evaluation of a polynomial at an element of a K-algebra. This is Definition 7.5.6 (def.pol.subs).

Given a polynomial f ∈ K[X] and an element a of a K-algebra A, we define f[a] := Σ_{n ∈ ℕ} f_n · a^n.

The sum is essentially finite since f is a polynomial (only finitely many coefficients are nonzero).

In Mathlib, this is implemented as Polynomial.aeval a f.

Equations

• FPS.polyEval f a = (Polynomial.aeval a) f

def FPS.«term_⦃_⦄» : Lean.TrailingParserDescr

Notation for polynomial evaluation: f⦃a⦄ means the value of f at a. This corresponds to the book's notation f[a].

Equations

• One or more equations did not get rendered due to their size.

theorem FPS.eval_def {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) (a : A) : polyEval f a = f.sum fun (n : ℕ) (c : K) => (algebraMap K A) c * a ^ n

Evaluation of a polynomial at an element of a K-algebra equals the sum Σ f_n · a^n. This is the explicit formula from Definition 7.5.6 (def.pol.subs).

theorem FPS.eval_eq_finsum {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) (a : A) : polyEval f a = ∑ n ∈ f.support, (algebraMap K A) (f.coeff n) * a ^ n

The evaluation f[a] can be written as a finite sum over the support of f. This makes explicit that the sum in Definition 7.5.6 is essentially finite.

theorem FPS.eval_eq_sum_range {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) (a : A) : polyEval f a = ∑ n ∈ Finset.range (f.natDegree + 1), (algebraMap K A) (f.coeff n) * a ^ n

Alternative formulation: f[a] = Σ_{n=0}^{deg f} f_n · a^n. This shows that the sum can be taken up to the degree.

Properties of Polynomial Evaluation

Theorem 7.5.7 (thm.pol.eval.a+b): Basic properties of evaluation.

theorem FPS.eval_add' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f g : Polynomial K) (a : A) : polyEval (f + g) a = polyEval f a + polyEval g a

(f + g)[a] = f[a] + g[a]. This is Theorem 7.5.7(a) in the source.

theorem FPS.eval_mul' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f g : Polynomial K) (a : A) : polyEval (f * g) a = polyEval f a * polyEval g a

(f * g)[a] = f[a] * g[a]. This is Theorem 7.5.7(a) in the source.

theorem FPS.eval_smul' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) (c : K) (a : A) : polyEval (c • f) a = c • polyEval f a

(c · f)[a] = c · f[a]. This is Theorem 7.5.7(b) in the source.

theorem FPS.eval_C' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (c : K) (a : A) : polyEval (Polynomial.C c) a = (algebraMap K A) c

C(c)[a] = c · 1_A. This is Theorem 7.5.7(c) in the source.

theorem FPS.eval_X' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (a : A) : polyEval Polynomial.X a = a

X[a] = a. This is Theorem 7.5.7(d) in the source.

theorem FPS.eval_X_pow' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (a : A) (i : ℕ) : polyEval (Polynomial.X ^ i) a = a ^ i

X^i[a] = a^i. This is Theorem 7.5.7(e) in the source.

theorem FPS.eval_comp' {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f g : Polynomial K) (a : A) : polyEval f (polyEval g a) = polyEval (f.comp g) a

f[g[a]] = (f ∘ g)[a], where f ∘ g denotes composition of polynomials. This is Theorem 7.5.7(f) in the source.

Examples and Special Cases

@[simp]

theorem FPS.isPolynomial_X {K : Type u_1} [CommRing K] : IsPolynomial PowerSeries.X

The polynomial X is a polynomial (in the FPS sense).

@[simp]

theorem FPS.isPolynomial_C {K : Type u_1} [CommRing K] (c : K) : IsPolynomial (PowerSeries.C c)

Any constant is a polynomial (in the FPS sense).

Special Evaluation Results

theorem FPS.eval_X_eq_self {K : Type u_1} [CommRing K] (f : Polynomial K) : polyEval f Polynomial.X = f

f[x] = f, i.e., evaluating at the indeterminate gives back the polynomial. This is noted after Definition 7.5.6 in the source.

theorem FPS.eval_zero_eq_coeff_zero {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) : polyEval f 0 = (algebraMap K A) (f.coeff 0)

f[0] = f₀, i.e., evaluating at 0 gives the constant term. This is noted after Definition 7.5.6 in the source.

theorem FPS.eval_one_eq_sum_coeffs {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] (f : Polynomial K) : polyEval f 1 = (algebraMap K A) (f.sum fun (x : ℕ) (c : K) => c)

f[1] = sum of all coefficients of f. This is noted after Definition 7.5.6 in the source.