Matrix.mul_mul_invOf_self_cancel
theorem Matrix.mul_mul_invOf_self_cancel :
∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
(A : Matrix m n α) (B : Matrix n n α) [inst_3 : Invertible B], A * B * ⅟B = A
This theorem, named `Matrix.mul_mul_invOf_self_cancel`, states that for any types `m`, `n`, and `α`, where `n` is a finite type and has a decidable equality, and `α` is a semiring, given a matrix `A` with entries in `α`, whose rows are indexed by `m` and columns by `n`, and a square matrix `B` with entries in `α` and both rows and columns indexed by `n`, if `B` is an invertible matrix, the product of `A`, `B`, and the inverse of `B` is equal to `A`. In other words, multiplying by a matrix and its inverse cancels out, leaving the original matrix, even when the matrices are rectangular instead of square.
More concisely: For any finite type `n` with decidable equality and semiring `α`, if `B` is an invertible square matrix with entries in `α` and indices matching those of rectangular matrix `A` with entries in `α`, then `A * B * B^⁻¹ = A`.
|
Matrix.mul_invOf_mul_self_cancel
theorem Matrix.mul_invOf_mul_self_cancel :
∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
(A : Matrix m n α) (B : Matrix n n α) [inst_3 : Invertible B], A * ⅟B * B = A
This theorem, `Matrix.mul_invOf_mul_self_cancel`, states that for any types `m`, `n`, and `α` representing the dimensions and entry type of a matrix, and for any two matrices `A` and `B` such that `A` is a `m` by `n` matrix and `B` is a square `n` by `n` matrix over a Semiring, if `B` is invertible, then the product of `A` and the inverse of `B` (`⅟B`) multiplied by `B` is equal to `A`. In mathematical notation, this would be expressed as `A * ⅟B * B = A`. This theorem is essentially a restatement of the property that multiplying a matrix by its inverse results in the identity, extended to the case of rectangular matrices where multiplication is defined.
More concisely: For any rectangular matrix `A` of dimensions `m` by `n` and any invertible square matrix `B` of dimensions `n` by `n` over a semiring, `A * B ^-1 * B = A`.
|
Matrix.invOf_mul_self_assoc
theorem Matrix.invOf_mul_self_assoc :
∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
(A : Matrix n n α) (B : Matrix n m α) [inst_3 : Invertible A], ⅟A * (A * B) = B
The theorem `Matrix.invOf_mul_self_assoc` states that for all types `m`, `n` and `α`, if `n` is a finite type, `n` has decidable equality, and `α` is a semiring. Given a square matrix `A` of type `Matrix n n α` and a rectangular matrix `B` of type `Matrix n m α`, such that `A` is invertible, then the product of the inverse of `A` (`⅟A`) and the product of `A` and `B` (`A * B`) equals `B`. In other words, when `A` is invertible, pre-multiplying `A * B` by `A`'s inverse results in `B`. This is a matrix version of the associativity of multiplication with the multiplicative inverse.
More concisely: For a square matrix `A` of type `Matrix n n α` over a semiring `α` with decidable equality and finite type `n`, if `A` is invertible, then `A⁻¹ * A * B = B` for any rectangular matrix `B` of type `Matrix n m α`.
|
Matrix.mul_invOf_self_assoc
theorem Matrix.mul_invOf_self_assoc :
∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
(A : Matrix n n α) (B : Matrix n m α) [inst_3 : Invertible A], A * (⅟A * B) = B
This theorem, 'Matrix.mul_invOf_self_assoc', states that for any types `m`, `n` and `α`, given a finite type `n`, decidable equality on `n`, and a semiring structure on `α`, for any square matrix `A` of size `n x n` with entries taken from `α` and any matrix `B` of size `n x m` with entries also taken from `α`, if `A` is invertible, then the multiplication of `A` and the product of the inverse of `A` and `B` is equal to `B`. This is essentially asserting the property of a multiplicative inverse for square matrices in the context of a semiring; multiplying a matrix by its inverse (to its left or right) yields the identity matrix, and further multiplying by any other compatible matrix leaves that matrix unchanged.
More concisely: For any square, invertible matrix A of size n x n over a semiring with finite type index n and decidable equality, and any matrix B of size n x m over the same semiring, A \* (A^(-1) \* B) = B holds.
|