Quadratic expressions in modules

Three-term expressions of the form x₀ + t • x₁ + t ^ 2 • x₂ occur in root-exponential actions. The lemmas here preserve these formulas under coefficientwise equality and linear maps, allowing root-exponential expressions to be compared after changing modules.

theorem TauCeti.quadraticPolynomial_congr {A : Type u_1} {M : Type u_2} [Semiring A] [AddCommMonoid M] [Module A M] {x₀ x₁ x₂ y₀ y₁ y₂ : M} (t : A) (h₀ : x₀ = y₀) (h₁ : x₁ = y₁) (h₂ : x₂ = y₂) : x₀ + t • x₁ + t ^ 2 • x₂ = y₀ + t • y₁ + t ^ 2 • y₂

Equal coefficients give equal quadratic expressions.

theorem LinearMap.map_quadraticPolynomial {A : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring A] [AddCommMonoid M] [Module A M] [AddCommMonoid N] [Module A N] (f : M →ₗ[A] N) (t : A) (x₀ x₁ x₂ : M) : f (x₀ + t • x₁ + t ^ 2 • x₂) = f x₀ + t • f x₁ + t ^ 2 • f x₂

A linear map commutes with evaluation of a quadratic expression.