represents_iff — Mathlib

English

An A with respect to b represents f if and only if, for every x, the coordinate expression matches f on the coordinate expression of x.

Русский

Матрица A относительно b представляет отображение f тогда и только тогда, когда для каждого x коэффициенты совпадают с f на коэффициентах x.

LaTeX

$$$A.Represents\\, b\\, f \\iff \\forall x,\\ Fintype.linearCombination(R,b)(A\\cdot_V x) = f(Fintype.linearCombination(R,b)(x))$$$

Lean4

theorem represents_iff {A : Matrix ι ι R} {f : Module.End R M} :
    A.Represents b f ↔ ∀ x, Fintype.linearCombination R b (A *ᵥ x) = f (Fintype.linearCombination R b x) :=
  ⟨fun e x => e.congr_fun x, fun H => LinearMap.ext fun x => H x⟩

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