Theorems · Theorem · linear algebra

Matrix.map_mul_intCast

∀ {n : Type u_2} [inst : Fintype n] {α : Type u_3} [inst_1 : NonAssocRing α] (A B : Matrix n n ℤ),
  (A * B).map Int.cast = A.map Int.cast * B.map Int.cast

Defined in

Mathlib.LinearAlgebra.Matrix.Integer

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeNonAssocRing