eq_of_smul_apply_eq_smul_apply — Mathlib

English

LinearIndependent eq_of_smul_apply_eq_smul_apply: if c • v i = d • v j with c ≠ 0, then i = j.

Русский

Если c • v_i = d • v_j и c ≠ 0, то i = j для линейно независимого множества.

LaTeX

$$Eq i j$$

Lean4

/-- Linear independent families are injective, even if you multiply either side. -/
theorem eq_of_smul_apply_eq_smul_apply {M : Type*} [AddCommMonoid M] [Module R M] {v : ι → M}
    (li : LinearIndependent R v) (c d : R) (i j : ι) (hc : c ≠ 0) (h : c • v i = d • v j) : i = j :=
  by
  have h_single_eq : Finsupp.single i c = Finsupp.single j d := li <| by simpa [Finsupp.linearCombination_apply] using h
  rcases (Finsupp.single_eq_single_iff ..).mp h_single_eq with (⟨H, _⟩ | ⟨hc, _⟩)
  · exact H
  · contradiction

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