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χ₂