injOn_genWeightSpace — Mathlib

English

The map χ ↦ genWeightSpace M χ is injective on the subset {χ | genWeightSpace M χ ≠ ⊥}.

Русский

Отображение χ ↦ genWeightSpace(M, χ) инъективно на области {χ | genWeightSpace M χ ≠ ⊥}.

LaTeX

$$InjOn (fun χ => genWeightSpace M χ) {χ | genWeightSpace M χ ≠ ⊥}$$

Lean4

theorem injOn_genWeightSpace [NoZeroSMulDivisors R M] :
    InjOn (fun (χ : L → R) ↦ genWeightSpace M χ) {χ | genWeightSpace M χ ≠ ⊥} :=
  by
  rintro χ₁ _ χ₂ hχ₂ (hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂)
  contrapose! hχ₂
  simpa [hχ₁₂] using disjoint_genWeightSpace R L M hχ₂

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