toMvPolynomial_totalDegree_le — Mathlib

English

For a linear map f and index i, the total degree of f.toMvPolynomial b1 b2 i is at most 1.

Русский

Для линейного отображения f и индекса i общая степень mv-полинома f.toMvPolynomial b1 b2 i не превышает 1.

LaTeX

$$((f.toMvPolynomial b1 b2 i).totalDegree) ≤ 1$$

Lean4

theorem toMvPolynomial_totalDegree_le (f : M₁ →ₗ[R] M₂) (i : ι₂) : (f.toMvPolynomial b₁ b₂ i).totalDegree ≤ 1 :=
  Matrix.toMvPolynomial_totalDegree_le _ _

Похожие утверждения