pairing_one_four_iff — Mathlib

English

If the sum of two roots lies in the root range, then a specific LI holds for the pair (as in LI from add_mem_range_root).

Русский

Если сумма корней лежит в диапазоне корня, то выполняется требуемая линейная независимость пары.

LaTeX

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

Lean4

/-- See also `RootPairing.pairingIn_one_four_iff`. -/
@[simp]
theorem pairing_one_four_iff [IsDomain R] : P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = (2 : R) • P.root i :=
  P.pairing_one_four_iff' i j <| smul_right_injective R two_ne_zero

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