linearIndependent_X — Mathlib

English

The family X_i (i ∈ σ) is linearly independent in MvPolynomial σ R.

Русский

Семейство X_i (i ∈ σ) линейно независимо в MvPolynomial(σ,R).

LaTeX

$$$\\text{linearIndependent}_R(\\,X: σ \\to \\mathrm{MvPolynomial}(σ,R)\\,)$$$

Lean4

theorem linearIndependent_X : LinearIndependent R (X : σ → MvPolynomial σ R) :=
  (basisMonomials σ R).linearIndependent.comp (fun s : σ => Finsupp.single s 1)
    (Finsupp.single_left_injective one_ne_zero)

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