disjoint_genWeightSpaceOf — Mathlib

English

If χ1 ≠ χ2 and R is NoZeroSMulDivisors on M, then genWeightSpace M χ1 and genWeightSpace M χ2 are disjoint.

Русский

Если χ1 ≠ χ2 и R имеет свойство NoZeroSMulDivisors на M, то genWeightSpace(M, χ1) и genWeightSpace(M, χ2) не пересекаются.

LaTeX

$$Disjoint (genWeightSpace M χ1) (genWeightSpace M χ2)$$

Lean4

theorem disjoint_genWeightSpaceOf [NoZeroSMulDivisors R M] {x : L} {φ₁ φ₂ : R} (h : φ₁ ≠ φ₂) :
    Disjoint (genWeightSpaceOf M φ₁ x) (genWeightSpaceOf M φ₂ x) :=
  by
  rw [← LieSubmodule.disjoint_toSubmodule]
  dsimp [genWeightSpaceOf]
  exact Module.End.disjoint_genEigenspace _ h _ _

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