reflectRoot_isNonZero — Mathlib

English

If β is a nonzero weight, then the reflected root α' = reflectRoot(α,β) is also nonzero.

Русский

Если β ненулевой вес, то отражённый корень α' = reflectRoot(α,β) тоже ненулевой.

LaTeX

$$$\beta \neq 0 \Rightarrow (\operatorname{reflectRoot}(\alpha,\beta)) \neq 0$$$

Lean4

theorem reflectRoot_isNonZero (α β : Weight K H L) (hβ : β.IsNonZero) : (reflectRoot α β).IsNonZero :=
  by
  intro e
  have : β (coroot α) = 0 := by
    by_cases hα : α.IsZero
    · simp [coroot_eq_zero_iff.mpr hα]
    simpa [root_apply_coroot hα, mul_two] using congr_fun (sub_eq_zero.mp e) (coroot α)
  have : reflectRoot α β = β := by ext; simp [reflectRoot, this]
  exact hβ (this ▸ e)

Похожие утверждения