Theorems · Definition · linear algebra

Matrix.Nonsingular

{n : Type u_1} → {R : Type u_3} → [Fintype n] → [DecidableEq n] → [CommSemiring R] → Matrix n n R → Prop

A square matrix A over a commutative semiring R is called nonsingular if it is only determinant balanced with respect to equal elements. See also See also Matrix.Nondegenerate.

Defined in

Mathlib.LinearAlgebra.Matrix.SemiringInverse

Cited by

27 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommSemiring