English
If A represents f with respect to b, then for any x, the coordinate expression given by A acting on x equals f applied to the coordinate expression of x.
Русский
Если матрица A представляет линейное отображение f относительно набора b, то для любого x выполняется равенство координатных выражений: A·x = f(x).
LaTeX
$$$\\forall x,\\; Fintype.linearCombination(R,b)(A\\cdot_V x) = f\\big(Fintype.linearCombination(R,b)(x)\\big)$$$
Lean4
/-- We say that a matrix represents an endomorphism of `M` if the matrix acting on `ι → R` is
equal to `f` via the projection `(ι → R) →ₗ[R] M` given by a fixed (spanning) set. -/
def Represents (A : Matrix ι ι R) (f : Module.End R M) : Prop :=
PiToModule.fromMatrix R b A = PiToModule.fromEnd R b f
