English
If notLinInd, then pairing j i acts on root i to produce twice root j, with a derived relation between coroots.
Русский
Если не линейная независимость, то сопряжение j i действует на корень i, давая удвоенный корень j; получаются связи через корoot.
LaTeX
$$$$ \\text{If } \\neg \\operatorname{LI}_R(\\![P.root i, P.root j]\\!), \\; P.pairing j i \\cdot P.root i = 2 \\cdot P.root j. $$$$
Lean4
theorem pairing_smul_root_eq_of_not_linearIndependent [NeZero (2 : R)] [NoZeroSMulDivisors R M]
(h : ¬LinearIndependent R ![P.root i, P.root j]) : P.pairing j i • P.root i = (2 : R) • P.root j :=
by
rw [LinearIndependent.pair_iff] at h
push_neg at h
obtain ⟨s, t, h₁, h₂⟩ := h
replace h₂ : s ≠ 0 := by
rcases eq_or_ne s 0 with rfl | hs
· exact False.elim <| h₂ rfl <| (smul_eq_zero_iff_left <| P.ne_zero j).mp <| by simpa using h₁
· assumption
have h₃ : t ≠ 0 := by
rcases eq_or_ne t 0 with rfl | ht
· exact False.elim <| h₂ <| (smul_eq_zero_iff_left <| P.ne_zero i).mp <| by simpa using h₁
· assumption
replace h₁ : s • P.root i = -t • P.root j := by rwa [← eq_neg_iff_add_eq_zero, ← neg_smul] at h₁
have h₄ : s * 2 = -(t * P.pairing j i) := by simpa using congr_arg (P.coroot' i) h₁
replace h₁ : (2 : R) • (s • P.root i) = (2 : R) • (-t • P.root j) := by rw [h₁]
rw [smul_smul, mul_comm, h₄, smul_comm, ← neg_mul, ← smul_smul] at h₁
exact smul_right_injective M (neg_ne_zero.mpr h₃) h₁
