English
A stronger variant: equivalence uses sums with coefficients A i j and basis elements b_i to recover f(b_j).
Русский
Усиленный вариант эквивалентности: сумма по i с коэффициентами A i j и базисными векторами восстанавливает f(b_j).
LaTeX
$$$A.Represents\\, b\\, f \\iff \\forall j, \\sum_i A_{ij}\\, b_i = f(b_j)$$$
Lean4
theorem represents_iff' {A : Matrix ι ι R} {f : Module.End R M} :
A.Represents b f ↔ ∀ j, ∑ i : ι, A i j • b i = f (b j) :=
by
constructor
· intro h i
have := LinearMap.congr_fun h (Pi.single i 1)
rwa [PiToModule.fromEnd_apply_single_one, PiToModule.fromMatrix_apply_single_one] at this
· intro h
ext
simp_rw [LinearMap.comp_apply, LinearMap.coe_single, PiToModule.fromEnd_apply_single_one,
PiToModule.fromMatrix_apply_single_one]
apply h
