Theorems · Theorem · linear algebra

Matrix.map_mul_ratCast

∀ {n : Type u_2} [inst : Fintype n] {α : Type u_3} [inst_1 : DivisionRing α] [CharZero α] (A B : Matrix n n ℚ),
  (A * B).map Rat.cast = A.map Rat.cast * B.map Rat.cast

Defined in

Mathlib.LinearAlgebra.Matrix.Integer

Cited by

0 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDivisionRingCharZero