English
For every i, the root P.root i is contained in the set allRoots P.
Русский
Для каждого i корень P.root i принадлежит allRoots P.
LaTeX
$$P.root i ∈ allRoots P$$
Lean4
theorem mem_allRoots (i : ι) : P.root i ∈ allRoots P :=
by
by_contra hi
obtain ⟨h₁, h₂⟩ := isOrthogonal_short_and_long P hi
have : Fintype ι := Fintype.ofFinite ι
have B := (P.posRootForm ℤ).toInvariantForm
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
rw [isOrthogonal_iff_pairing_eq_zero, ← B.apply_root_root_zero_iff] at h₁ h₂
have key : B.form (P.root i) = 0 := by
ext x
have hx : x ∈ span R {longRoot P, shortRoot P} := by simp
simp only [LinearMap.zero_apply]
induction hx using Submodule.span_induction with
| zero => simp
| mem => aesop
| add => simp_all
| smul => simp_all
simpa using LinearMap.congr_fun key (P.root i)
