Mathlib Map

Theorems · Definition · linear algebra

Matrix.detInvertibleOfLeftInverse

{n : Type u'} →
  {α : Type v} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] → [inst_2 : CommRing α] → (A B : Matrix n n α) → B * A = 1 → Invertible A.det

A.det is invertible if A has a left inverse.

Defined in
Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Cited by
0 results in Mathlib
Foundations
Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FintypeDecidableEqCommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Matrix.detInvertibleOfInvertible · cited by 3Matrix.detInvertibleOfInv…CommRing · cited by 17173CommRingFintype · cited by 7736FintypeMatrix · cited by 4303MatrixMatrix.det · cited by 665Matrix.detInvertible · cited by 549InvertibleMatrix.detInvertibleOfLeftInv…CITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • CommRingstatement and proof · cited by 17,173
  • Fintypestatement and proof · cited by 7,736
  • Matrixstatement and proof · cited by 4,303
  • Matrix.detstatement and proof · cited by 665
  • Invertiblestatement · cited by 549

Cited by1

Results whose statement or proof uses this declaration.