Theorems · Theorem · linear algebra

Matrix.inv_mulVec_eq_vec

∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A : Matrix n n α}
  [Invertible A] {u v : n → α}, u = A.mulVec v → A⁻¹.mulVec u = v

Defined in

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommRingInvertible