map_mul_ratCast — Mathlib

English

Casting rationals to a division ring α commutes with matrix multiplication: map (A * B) (Rat.castHom α) = map A (Rat.cast α) * map B (Rat.cast α).

Русский

Преобразование дробей в деление α сохраняет умножение матриц: map(A B) = map(A) map(B).

LaTeX

$$$$ (A \\cdot B)^{\\text{cast}} = A^{\\text{cast}} \\cdot B^{\\text{cast}}, \\quad A,B \\in M_n(\\mathbb{Q}). $$$$

Lean4

theorem map_mul_ratCast {α : Type*} [DivisionRing α] [CharZero α] (A B : Matrix n n ℚ) :
    map (A * B) ((↑) : ℚ → α) = map A (↑) * map B (↑) :=
  Matrix.map_mul (f := Rat.castHom α)

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