English
Casting integers entrywise to a ring α preserves matrix multiplication: map (A * B) with Int.cast equals map A with Int.cast times map B with Int.cast.
Русский
Преобразование целых чисел поэлементно в кольцо α сохраняет умножение матриц: map(A B) = map A · map B.
LaTeX
$$$$ (A \\cdot B)^{\\uparrow} = A^{\\uparrow} \\cdot B^{\\uparrow}, \\quad A,B \\in M_n(\\mathbb{Z}), $$$$
Lean4
theorem map_mul_intCast {α : Type*} [NonAssocRing α] (A B : Matrix n n ℤ) :
map (A * B) ((↑) : ℤ → α) = map A (↑) * map B (↑) :=
Matrix.map_mul (f := Int.castRingHom α)