def Hex.Matrix.inverse? {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n : Nat} (A : Matrix F n n) : Option (Matrix F n n)

Invert a square matrix by reducing its coefficient block and accumulating the same row operations on the identity. Failure means singularity.

Equations

• A.inverse? = if A.rowReduce.rank = n then some A.rowReduce.transform else none

theorem Hex.Matrix.inverse?_isSome {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n : Nat} (A : Matrix F n n) : A.inverse?.isSome = true ↔ A.rowReduce_rank = n

Inversion succeeds exactly at full rank.

theorem Hex.Matrix.inverse?_eq_none {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n : Nat} (A : Matrix F n n) : A.inverse? = none ↔ A.rowReduce_rank ≠ n

Inversion fails exactly when the matrix is rank deficient.

theorem Hex.Matrix.inverse?_spec {F : Type u} [Lean.Grind.Field F] [DecidableEq F] {n : Nat} (A B : Matrix F n n) : A.inverse? = some B → A * B = Matrix.identity n ∧ B * A = Matrix.identity n

The returned matrix is a two-sided inverse.

theorem Hex.Matrix.inverse?_empty {F : Type u} [Lean.Grind.Field F] [DecidableEq F] (A : Matrix F 0 0) : A.inverse? = some (Matrix.identity 0)

The empty matrix has the empty identity as its inverse.