Nonsingular inverses over semirings #

This file proves A * B = 1 ↔ B * A = 1 for square matrices over a commutative semiring.

def Matrix.detp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤˣ) (A : Matrix n n R) :

The determinant, but only the terms of a given sign.

Instances For

source

📐 coverage

@[simp]

theorem Matrix.detp_one_diagonal {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (d : n → R) :

detp 1 (diagonal d) = ∏ i : n, d i

source

📐 coverage

@[simp]

theorem Matrix.detp_one_one {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] :

detp 1 1 = 1

source

📐 coverage

@[simp]

theorem Matrix.detp_neg_one_diagonal {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (d : n → R) :

detp (-1) (diagonal d) = 0

source

📐 coverage

@[simp]

theorem Matrix.detp_neg_one_one {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] :

detp (-1) 1 = 0

source

🔸 coverage

def Matrix.adjp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤˣ) (A : Matrix n n R) :

Matrix n n R

The adjugate matrix, but only the terms of a given sign.

Instances For

source

📐 coverage

theorem Matrix.adjp_apply {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤˣ) (A : Matrix n n R) (i j : n) :

adjp s A i j = ∑ σ ∈ Equiv.Perm.ofSign s with σ j = i, ∏ k ∈ {j}ᶜ, A k (σ k)

source

📐 coverage

theorem Matrix.detp_mul {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A B : Matrix n n R) :

detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

source

📐 coverage

theorem Matrix.mul_adjp_apply_eq {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤˣ) (A : Matrix n n R) (i : n) :

(A * adjp s A) i i = detp s A

source

📐 coverage

theorem Matrix.mul_adjp_apply_ne {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) (i j : n) (h : i ≠ j) :

(A * adjp 1 A) i j = (A * adjp (-1) A) i j

source

📐 coverage

theorem Matrix.mul_adjp_add_detp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) :

A * adjp 1 A + detp (-1) A • 1 = A * adjp (-1) A + detp 1 A • 1

source

📐 coverage

theorem Matrix.isAddUnit_mul {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} {d : n → R} (hAB : A * B = diagonal d) (i j k : n) (hij : i ≠ j) :

IsAddUnit (A i k * B k j)

source

📐 coverage

theorem Matrix.isAddUnit_detp_mul_detp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} {d : n → R} (hAB : A * B = diagonal d) :

IsAddUnit (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)

source

📐 coverage

theorem Matrix.isAddUnit_detp_smul_mul_adjp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} {d : n → R} (hAB : A * B = diagonal d) :

IsAddUnit (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B))

source

📐 coverage

theorem Matrix.detp_smul_add_adjp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} (hAB : A * B = 1) :

detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

source

📐 coverage

theorem Matrix.detp_smul_adjp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} (hAB : A * B = 1) :

A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B

source

📐 coverage

@[instance 100]

instance Matrix.instIsStablyFiniteRingOfCommSemiring {R : Type u_3} [CommSemiring R] :

IsStablyFiniteRing R

source

📐 coverage

@[deprecated mul_eq_one_comm (since := "2025-11-29")]

theorem Matrix.mul_eq_one_comm {M : Type u_2} [MulOne M] [IsDedekindFiniteMonoid M] {a b : M} :

a * b = 1 ↔ b * a = 1

Alias of mul_eq_one_comm.

source

🔸 coverage

@[implicit_reducible, deprecated invertibleOfLeftInverse (since := "2025-12-06")]

def Matrix.invertibleOfLeftInverse {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A B : Matrix n n R) (h : B * A = 1) :

Invertible A

We can construct an instance of invertible A if A has a left inverse.

Instances For

source

🔸 coverage

@[implicit_reducible, deprecated invertibleOfRightInverse (since := "2025-12-06")]

def Matrix.invertibleOfRightInverse {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A B : Matrix n n R) (h : A * B = 1) :

Invertible A

We can construct an instance of invertible A if A has a right inverse.

Instances For

source

📐 coverage

@[deprecated IsUnit.of_mul_eq_one_right (since := "2025-12-06")]

theorem Matrix.isUnit_of_left_inverse {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} (h : B * A = 1) :

IsUnit A

source

📐 coverage

@[deprecated isUnit_iff_exists_inv' (since := "2025-12-06")]

theorem Matrix.exists_left_inverse_iff_isUnit {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} :

(∃ (B : Matrix n n R), B * A = 1) ↔ IsUnit A

source

📐 coverage

@[deprecated IsUnit.of_mul_eq_one (since := "2025-12-06")]

theorem Matrix.isUnit_of_right_inverse {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} (h : A * B = 1) :

IsUnit A

source

📐 coverage

@[deprecated isUnit_iff_exists_inv (since := "2025-12-06")]

theorem Matrix.exists_right_inverse_iff_isUnit {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} :

(∃ (B : Matrix n n R), A * B = 1) ↔ IsUnit A

Documentation

Mathlib.LinearAlgebra.Matrix.SemiringInverse

Nonsingular inverses over semirings #