isReduced_iff' — Mathlib

English

For a RootPairing P, the reduced property is characterized by a condition on all pairs of indices: if i ≠ j and the two root vectors are not linearly independent, then the two roots are negatives of each other.

Русский

Для парирования корней P свойство редукции определяется по любым парам индексов: если i ≠ j и корневые векторы не линейно независимы, то один корень равен минусу другого.

LaTeX

$$$$ P.IsReduced \\iff \\forall i,j,\\; i \\neq j \\rightarrow \\bigl( \\neg \\operatorname{LI}_R(\\![P.root i, P.root j]\\!) \\rightarrow P.root i = -P.root j \\bigr). $$$$

Lean4

theorem isReduced_iff' :
    P.IsReduced ↔ ∀ i j : ι, i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j :=
  by
  rw [isReduced_iff]
  refine ⟨fun h i j hij hLin ↦ ?_, fun h i j hLin ↦ ?_⟩
  · specialize h i j hLin
    simp_all only [ne_eq, EmbeddingLike.apply_eq_iff_eq, false_or]
  · rcases eq_or_ne i j with rfl | h'
    · tauto
    · exact Or.inr (h i j h' hLin)

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