Theorems · Definition · linear algebra

Matrix.toMvPolynomial

{m : Type u_1} →
  {n : Type u_2} → {R : Type u_4} → [Fintype n] → [inst : CommSemiring R] → Matrix m n R → m → MvPolynomial n R

Let M be an (m × n)-matrix over R. Then Matrix.toMvPolynomial M is the family (indexed by i : m) of multivariate polynomials in n variables over R that evaluates on c : n → R to the dot product of the i-th row of M with c: Matrix.toMvPolynomial M i is the sum of the monomials C (M i j) * X j.

Defined in

Mathlib.Algebra.Module.LinearMap.Polynomial

Cited by

14 results in Mathlib

Foundations

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

Assumes

FintypeCommSemiring