English
If two RootSystems are crystallographic and reduced, there exists an equivalence that maps the weight bases and respects the Cartan matrices along a bijection of supports.
Русский
Если две Корневые системы кристаллические и редуцируемые, существует эквивалент, который отображает базы весов и сохраняет Картановы матрицы через биекцию опор.
LaTeX
$$equivOfCartanMatrixEq ...$$
Lean4
/-- If `α = P.root i` and `β = P.root j` are linearly independent, this is the value `p ≥ 0` where
`β - q • α, ..., β - α, β, β + α, ..., β + p • α` is the `α`-chain through `β`.
In the absence of linear independence, it takes a junk value. -/
def chainTopCoeff : ℕ :=
if h : LinearIndependent R ![P.root i, P.root j] then
(P.setOf_root_add_zsmul_eq_Icc_of_linearIndependent h).choose_spec.2.choose.toNat
else 0
