mathlib3 documentation

data.matrix.invertible

Extra lemmas about invertible matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Many of the invertible lemmas are about *; this restates them to be about ⬝.

For lemmas about the matrix inverse in terms of the determinant and adjugate, see matrix.has_inv in linear_algebra/matrix/nonsingular_inverse.lean.

source
@[protected]
theorem matrix.inv_of_mul_self {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (A : matrix n n α) [invertible A] :
(⅟ A).mul A = 1

A copy of inv_of_mul_self using ⬝ not *.

source
@[protected]
theorem matrix.mul_inv_of_self {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (A : matrix n n α) [invertible A] :
A.mul (⅟ A) = 1

A copy of mul_inv_of_self using ⬝ not *.

source
@[protected]
theorem matrix.inv_of_mul_self_assoc {m : Type u_1} {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (A : matrix n n α) (B : matrix n m α) [invertible A] :
(⅟ A).mul (A.mul B) = B

A copy of inv_of_mul_self_assoc using ⬝ not *.

source
@[protected]
theorem matrix.mul_inv_of_self_assoc {m : Type u_1} {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (A : matrix n n α) (B : matrix n m α) [invertible A] :
A.mul ((⅟ A).mul B) = B

A copy of mul_inv_of_self_assoc using ⬝ not *.

source
@[protected]
theorem matrix.mul_inv_of_mul_self_cancel {m : Type u_1} {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (A : matrix m n α) (B : matrix n n α) [invertible B] :
(A.mul (⅟ B)).mul B = A

A copy of mul_inv_of_mul_self_cancel using ⬝ not *.

source
@[protected]
theorem matrix.mul_mul_inv_of_self_cancel {m : Type u_1} {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (A : matrix m n α) (B : matrix n n α) [invertible B] :
(A.mul B).mul (⅟ B) = A

A copy of mul_mul_inv_of_self_cancel using ⬝ not *.

source
@[protected, reducible]
def matrix.invertible_mul {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (A B : matrix n n α) [invertible A] [invertible B] :
invertible (A.mul B)

A copy of invertible_mul using ⬝ not *.

Equations
source
@[reducible]
def invertible.matrix_mul {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] {A B : matrix n n α} (ha : invertible A) (hb : invertible B) :
invertible (A.mul B)

A copy of invertible.mul using ⬝ not *.

Equations
source
@[protected]
theorem matrix.inv_of_mul {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] {A B : matrix n n α} [invertible A] [invertible B] [invertible (A.mul B)] :
⅟ (A.mul B) = (⅟ B).mul (⅟ A)
source
@[protected, reducible]
def matrix.invertible_of_invertible_mul {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (a b : matrix n n α) [invertible a] [invertible (a.mul b)] :
invertible b

A copy of invertible_of_invertible_mul using ⬝ not *.

Equations
source
@[protected, reducible]
def matrix.invertible_of_mul_invertible {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (a b : matrix n n α) [invertible (a.mul b)] [invertible b] :
invertible a

A copy of invertible_of_mul_invertible using ⬝ not *.

Equations
source
@[reducible]
def invertible.matrix_mul_left {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] {a : matrix n n α} (ha : invertible a) (b : matrix n n α) :
invertible b ≃ invertible (a.mul b)

A copy of invertible.mul_left using ⬝ not *.

Equations
source
@[reducible]
def invertible.matrix_mul_right {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (a : matrix n n α) {b : matrix n n α} (ha : invertible b) :
invertible a ≃ invertible (a.mul b)

A copy of invertible.mul_right using ⬝ not *.

Equations