map_mul_intCast — Mathlib

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 α)

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