coroot_eq_zero_iff — Mathlib

English

For a nonzero root α, the root space has dimension one.

Русский

Для ненулевого корня α размерность корневого пространства равна единице.

LaTeX

$$finrank_K(rootSpace(H,α)) = 1$$

Lean4

@[simp]
theorem coroot_eq_zero_iff {α : Weight K H L} : coroot α = 0 ↔ α.IsZero :=
  by
  refine ⟨fun hα ↦ ?_, fun hα ↦ ?_⟩
  · by_contra contra
    simpa [hα, ← α.coe_coe, map_zero] using root_apply_coroot contra
  · simp [coroot, Weight.coe_toLinear_eq_zero_iff.mpr hα]

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