English
Let R be a commutative ring and M a matrix with respect to bases v1,v2. For x ∈ M1, the image A.toLin v1 v2 x equals 0 if and only if all coordinates of x in the basis v1 vanish after applying A, i.e., (A *ᵥ v1.repr x)_j = 0 for all j.
Русский
Пусть R — коммутативное кольцо, A — матрица, имеющая базисы v1,v2. Для x ∈ M1 отображение A.toLin v1 v2 x равно 0 тогда и только тогда, когда все координаты x по базису v1 переходят в нуль после применения A: (A *ᵥ v1.repr x)_j = 0 для всех j.
LaTeX
$$$\\Big( A.toLin\,v_1\,v_2\,x = 0 \\Big) \\iff \\forall j, \\big( A \\cdot_{v_1} (v_1\\.repr\\,x) \\big)_j = 0$$$
Lean4
theorem toLin_apply_eq_zero_iff {R M₁ M₂ : Type*} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁]
[Module R M₂] {v₁ : Basis n R M₁} {v₂ : Basis m R M₂} {A : Matrix m n R} {x : M₁} :
A.toLin v₁ v₂ x = 0 ↔ ∀ j, (A *ᵥ v₁.repr x) j = 0 :=
by
rw [toLin_apply]
exact ⟨Fintype.linearIndependent_iff.mp v₂.linearIndependent _, fun h ↦ by simp [h]⟩
