English
Mapping a function f distributes over the construction of a matrix partitioned by columns: map f (fromCols(A1,A2)) = fromCols(map f A1, map f A2).
Русский
Отображение по функции f распространяется на разбиение матрицы по столбцам: map f (fromCols(A1,A2)) = fromCols(map f A1, map f A2).
LaTeX
$$$$ (\operatorname{fromCols}(A_1,A_2)).\operatorname{map} f = \operatorname{fromCols}(A_1.\operatorname{map} f)(A_2.\operatorname{map} f). $$$$
Lean4
theorem fromCols_map (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) {R' : Type*} (f : R → R') :
(fromCols A₁ A₂).map f = fromCols (A₁.map f) (A₂.map f) := by ext _ (_ | _) <;> rfl