English
The induction_on_cartanMatrix theorem proves the connectedness property by inductively stepping through roots connected by nonzero Cartan entries, using reflections in invtSubmodule to propagate the property.
Русский
Теорема induction_on_cartanMatrix доказывает связность, пошагово перемещая свойство по корням, связанным ненулевыми записями Картона, с помощью отражений иinvSubmodule.
LaTeX
$$Inductive propagation along nonzero Cartan entries$$
Lean4
theorem root_add_nsmul_mem_range_iff_le_chainTopCoeff {n : ℕ} :
P.root j + n • P.root i ∈ range P.root ↔ n ≤ P.chainTopCoeff i j :=
by
set S : Set ℤ := {z | P.root j + z • P.root i ∈ range P.root} with S_def
suffices (n : ℤ) ∈ S ↔ n ≤ P.chainTopCoeff i j by simpa only [S_def, mem_setOf_eq, natCast_zsmul] using this
have aux : P.chainTopCoeff i j = (P.setOf_root_add_zsmul_eq_Icc_of_linearIndependent h).choose_spec.2.choose.toNat :=
by simp [chainTopCoeff, h]
obtain ⟨hp, h₂ : S = _⟩ := (P.setOf_root_add_zsmul_eq_Icc_of_linearIndependent h).choose_spec.2.choose_spec
rw [aux, h₂, mem_Icc]
have := (P.setOf_root_add_zsmul_eq_Icc_of_linearIndependent h).choose_spec.1
cutsat
