root_apply_cartanEquivDual_symm_ne_zero

English

If α ≠ 0, then α((cartanEquivDual H)^{-1}(α)) ≠ 0.

Русский

Если α ≠ 0, то α((cartanEquivDual H)^{-1}(α)) ≠ 0.

LaTeX

$$$\alpha((\mathrm{cartanEquivDual} H)^{-1}(\alpha)) \neq 0$$$

Lean4

theorem root_apply_cartanEquivDual_symm_ne_zero {α : Weight K H L} (hα : α.IsNonZero) :
    α ((cartanEquivDual H).symm α) ≠ 0 := by
  contrapose! hα
  suffices (cartanEquivDual H).symm α ∈ α.ker ⊓ corootSpace α
    by
    rw [(disjoint_ker_weight_corootSpace α).eq_bot] at this
    simpa using this
  exact Submodule.mem_inf.mp ⟨hα, cartanEquivDual_symm_apply_mem_corootSpace α⟩

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