rootSpace_one_div_two_smul — Mathlib

English

If α is nonzero, then the root space at 2α is trivial: rootSpace H (2 • α) = ⊥.

Русский

Если α ≠ 0, то корневое пространство по 2α тривиально: rootSpace H (2α) = ⊥.

LaTeX

$$$\operatorname{rootSpace}(H, 2 \cdot α) = ⊥$$$

Lean4

theorem rootSpace_one_div_two_smul (hα : α.IsNonZero) : rootSpace H ((2⁻¹ : K) • α) = ⊥ :=
  by
  by_contra h
  let W : Weight K H L := ⟨_, h⟩
  have hW : 2 • (W : H → K) = α := by
    change 2 • (2⁻¹ : K) • (α : H → K) = α
    rw [← Nat.cast_smul_eq_nsmul K, smul_smul]; simp
  apply α.genWeightSpace_ne_bot
  have := rootSpace_two_smul W (fun (e : (W : H → K) = 0) ↦ hα <| by apply_fun (2 • ·) at e; simpa [hW] using e)
  rwa [hW] at this

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