eq_of_mem_smul_span_of_index_eq_index

English

If x,y ∈ (n)⁻¹ • L and index n x = index n y, then x = y.

Русский

Если x,y ∈ (n)⁻¹ • L и index n x = index n y, тогда x = y.

LaTeX

$$$$ x,y \in (n:\\mathbb{R})^{-1} \cdot L \;\wedge\; \mathrm{index}\, n\, x = \mathrm{index}\, n\, y \Rightarrow x = y $$$$

Lean4

theorem eq_of_mem_smul_span_of_index_eq_index {x y : ι → ℝ} (hx : x ∈ (n : ℝ)⁻¹ • L) (hy : y ∈ (n : ℝ)⁻¹ • L)
    (h : index n x = index n y) : x = y := by
  rw [← tag_index_eq_self_of_mem_smul_span n hx, ← tag_index_eq_self_of_mem_smul_span n hy, h]

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