English
For a reduced irreducible root system, either B.form(α_i, α_i) and B.form(α_j, α_j) are equal, or are multiples 2 or 3 of each other, with symmetric alternatives swapping i and j.
Русский
Для редуцированной нерелизируемой корневой системы либо значения B(α_i, α_i) и B(α_j, α_j) равны, либо один из них вдвое/в трое отличается от другого, с симметрией при обмене i и j.
LaTeX
$$$B(α_i, α_i) = B(α_j, α_j) \lor B(α_i, α_i) = 2 B(α_j, α_j) \lor B(α_i, α_i) = 3 B(α_j, α_j) \lor B(α_j, α_j) = 2 B(α_i, α_i) \lor B(α_j, α_j) = 3 B(α_i, α_i)$$$
Lean4
theorem isAnisotropic_of_isValuedIn (S : Type*) [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R]
[FaithfulSMul S R] [P.IsValuedIn S] : IsAnisotropic P
where
rootForm_root_ne_zero i := (P.posRootForm S).form_apply_root_ne_zero i
corootForm_coroot_ne_zero i := (P.flip.posRootForm S).form_apply_root_ne_zero i
