finrank_eq_zero — Mathlib

English

If σ is nonempty, the multivariate polynomial algebra MvPolynomial(σ,K) is infinite-dimensional over K; hence its finite rank is zero.

Русский

Если σ ненулевой, алгебра многочленов MvPolynomial(σ,K) над полем K бесконечно размерна; следовательно, её конечный ранг равен 0.

LaTeX

$$$\\operatorname{Module.finrank}_K\\bigl( \\mathrm{MvPolynomial}(\\sigma,K) \\bigr) = 0$$$

Lean4

theorem finrank_eq_zero [Nonempty σ] : Module.finrank K (MvPolynomial σ K) = 0 :=
  (basisMonomials σ K).linearIndependent.finrank_eq_zero_of_infinite

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