The homogeneous linear form ∑ i, a i * X i with a given coefficient vector, and its basic API: homogeneity, degree, evaluation, coefficient maps, renaming and linearity in the coefficient vector.

noncomputable def CCDN.linearForm {R : Type u_1} {σ : Type u_3} [CommSemiring R] [Fintype σ] (a : σ → R) : MvPolynomial σ R

The linear form ∑ i, a i * X i with coefficient vector a.

Equations

• CCDN.linearForm a = ∑ i : σ, MvPolynomial.C (a i) * MvPolynomial.X i

theorem CCDN.linearForm_isHomogeneous {R : Type u_1} {σ : Type u_3} [CommSemiring R] [Fintype σ] (a : σ → R) : (linearForm a).IsHomogeneous 1

A linear form is homogeneous of degree one.

theorem CCDN.linearForm_totalDegree_le {R : Type u_1} {σ : Type u_3} [CommSemiring R] [Fintype σ] (a : σ → R) : (linearForm a).totalDegree ≤ 1

A linear form has total degree at most one.

@[simp]

theorem CCDN.eval_linearForm {R : Type u_1} {σ : Type u_3} [CommSemiring R] [Fintype σ] (a x : σ → R) : (MvPolynomial.eval x) (linearForm a) = ∑ i : σ, a i * x i

The linear form with coefficients a evaluates at x to ∑ i, a i * x i.

@[simp]

theorem CCDN.aeval_linearForm {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [Fintype σ] [CommSemiring S] [Algebra R S] (a : σ → R) (x : σ → S) : (MvPolynomial.aeval x) (linearForm a) = ∑ i : σ, (algebraMap R S) (a i) * x i

The linear form with coefficients a evaluates at a point x of an R-algebra S to ∑ i, algebraMap R S (a i) * x i.

@[simp]

theorem CCDN.eval₂_linearForm {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [Fintype σ] [CommSemiring S] (φ : R →+* S) (a : σ → R) (x : σ → S) : MvPolynomial.eval₂ φ x (linearForm a) = ∑ i : σ, φ (a i) * x i

Evaluating the linear form with coefficients a along φ at x gives ∑ i, φ (a i) * x i.

theorem CCDN.rename_linearForm {R : Type u_1} {σ : Type u_3} {τ : Type u_4} [CommSemiring R] [Fintype σ] [Fintype τ] (e : σ ≃ τ) (a : σ → R) : (MvPolynomial.rename ⇑e) (linearForm a) = linearForm (a ∘ ⇑e.symm)

Renaming the variables of a linear form along a bijection e gives the linear form whose coefficient vector is reindexed by e.symm.

@[simp]

theorem CCDN.linearForm_zero {R : Type u_1} {σ : Type u_3} [CommSemiring R] [Fintype σ] : linearForm 0 = 0

The linear form with zero coefficient vector is zero.

theorem CCDN.linearForm_add {R : Type u_1} {σ : Type u_3} [CommSemiring R] [Fintype σ] (a b : σ → R) : linearForm (a + b) = linearForm a + linearForm b

The linear form is additive in its coefficient vector.

theorem CCDN.linearForm_smul {R : Type u_1} {σ : Type u_3} [CommSemiring R] [Fintype σ] (c : R) (a : σ → R) : linearForm (c • a) = c • linearForm a

The linear form commutes with scalar multiplication of its coefficient vector.

noncomputable def CCDN.linearFormLinearMap (R : Type u_1) (σ : Type u_3) [CommSemiring R] [Fintype σ] : (σ → R) →ₗ[R] MvPolynomial σ R

linearForm as a linear map from coefficient vectors to polynomials.

Equations

• CCDN.linearFormLinearMap R σ = { toFun := CCDN.linearForm, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CCDN.linearFormLinearMap_apply {R : Type u_1} {σ : Type u_3} [CommSemiring R] [Fintype σ] (a : σ → R) : (linearFormLinearMap R σ) a = linearForm a

The linear map linearFormLinearMap R σ sends a coefficient vector a to linearForm a.