disjoint_ker_weight_corootSpace — Mathlib

English

The weight kernel and coroot space intersect trivially.

Русский

Весовое ядро и коротовое пространство пересекаются только в нулевой подпрострастве.

LaTeX

$$Disjoint α.ker (coroot α) = ⊥$$

Lean4

theorem disjoint_ker_weight_corootSpace (α : Weight K H L) : Disjoint α.ker (corootSpace α) :=
  by
  rw [disjoint_iff]
  refine (Submodule.eq_bot_iff _).mpr fun x ⟨hαx, hx⟩ ↦ ?_
  replace hαx : α x = 0 := by simpa using hαx
  exact eq_zero_of_apply_eq_zero_of_mem_corootSpace x α hαx hx

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