basisUnique_repr_eq_zero_iff — Mathlib

English

For the basis constructed with basisUnique, the i-th coordinate of v is zero if and only if v = 0.

Русский

Для базиса, полученного через basisUnique, i-ая координата v равна нулю тогда и только тогда, когда v = 0.

LaTeX

$$$$ (\\text{basisUnique }\\iota\\;h).repr\\;v\\;i = 0 \\iff v = 0 $$$$

Lean4

@[simp]
theorem basisUnique_repr_eq_zero_iff {ι : Type*} [Unique ι] {h : finrank R M = 1} {v : M} {i : ι} :
    (basisUnique ι h).repr v i = 0 ↔ v = 0 :=
  ⟨fun hv => (basisUnique ι h).repr.map_eq_zero_iff.mp (Finsupp.ext fun j => Subsingleton.elim i j ▸ hv), fun hv => by
    rw [hv, LinearEquiv.map_zero, Finsupp.zero_apply]⟩

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