linearIndependent_of_add_mem_range_root'

English

Same as LI from_add_mem_range_root, but with a variant using reflection permutation, ensuring LI for P.root i and P.root (P.reflectionPerm j j).

Русский

То же самое, что и LI из add_mem_range_root, но с вариантом через отражение перестановки, обеспечивающим LI для P.root i и P.root (P.reflectionPerm j j).

LaTeX

$$$$ (P.root i + P.root j) \\in \\operatorname{range}(P.root) \\Rightarrow \\operatorname{LI}_R(\\![P.root i, P.root (P.reflectionPerm j j)]\\!). $$$$

Lean4

theorem linearIndependent_of_add_mem_range_root' [CharZero R] [IsDomain R] [P.IsReduced] {i j : ι}
    (h : P.root i + P.root j ∈ range P.root) : LinearIndependent R ![P.root i, P.root j] :=
  have : IsReflexive R M := .of_isPerfPair P.toLinearMap
  have _i : NoZeroSMulDivisors ℤ M := NoZeroSMulDivisors.int_of_charZero R M
  P.linearIndependent_of_add_mem_range_root h

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