linearIndependent — Mathlib

English

Under the reduced assumption, if i ≠ j and P.root i ≠ -P.root j, then the pair {P.root i, P.root j} is linearly independent.

Русский

При предположении редуцированности, если i ≠ j и P.root i ≠ -P.root j, то пара {P.root i, P.root j} линейно независима.

LaTeX

$$$$ [P.IsReduced] \\Rightarrow (i \\neq j) \\rightarrow (P.root i \\neq -P.root j) \\rightarrow \\operatorname{LI}_R(\\![P.root i, P.root j]\\!). $$$$

Lean4

theorem linearIndependent [P.IsReduced] (h : i ≠ j) (h' : P.root i ≠ -P.root j) :
    LinearIndependent R ![P.root i, P.root j] :=
  by
  have := IsReduced.eq_or_eq_neg (P := P) i j
  simp_all

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