English
Let f be a semilinear equivalence between modules α and β. Then the induced map on m×n matrices acts entrywise, and its associated linear map coincides with the map that applies f to every entry.
Русский
Пусть f — линейное эквивалент между модулями α и β. Тогда индуцированное отображение на матрицах размера m×n действует по каждому элементу, и связанная линейная карта совпадает с отображением, получаемым применением f к каждому элементу матрицы.
LaTeX
$$$\forall M=(a_{ij})\in M_{m\times n}(\alpha),\quad [(f.mapMatrix)(M)]_{ij} = f(a_{ij})\quad \text{для всех } i,j.$$$
Lean4
@[simp]
theorem mapMatrix_toLinearMap (f : α ≃ₛₗ[σᵣₛ] β) :
(f.mapMatrix : _ ≃ₛₗ[_] Matrix m n β).toLinearMap = f.toLinearMap.mapMatrix := by rfl
