toMvPolynomial_isHomogeneous — Mathlib

English

For any linear map f and index i, the multivariate polynomial f.toMvPolynomial b1 b2 i is homogeneous of degree 1.

Русский

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

LaTeX

$$(f.toMvPolynomial b1 b2 i).IsHomogeneous 1$$

Lean4

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

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