Theorems · Theorem · linear algebra

Matrix.inv_kronecker

∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (A : Matrix m m α) (B : Matrix n n α),
  (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B)⁻¹ = Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A⁻¹ B⁻¹

Defined in

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommRingFintypeDecidableEq