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) : R

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

@[simp]

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

@[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

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.

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)

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)

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

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

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

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

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} (hAB : A * B = 1) : IsAddUnit (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)

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} (hAB : A * B = 1) : IsAddUnit (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B))

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

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

@[instance 100]

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

@[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.

@[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.

@[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.

@[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

@[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

@[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

@[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