Matrix.zpow_add_one
theorem Matrix.zpow_add_one :
∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
{A : Matrix n' n' R}, IsUnit A.det → ∀ (n : ℤ), A ^ (n + 1) = A ^ n * A
The theorem `Matrix.zpow_add_one` states that for any type `n'` with decidable equality and finite cardinality, and any type `R` forming a commutative ring, given a square matrix `A` with elements of type `R` and indices of type `n'`, if the determinant of `A` is a unit (i.e., has a multiplicative inverse), then for any integer `n`, the `(n + 1)`-th power of `A` is equal to the `n`-th power of `A` multiplied by `A`. This in essence provides a recursive definition for calculating the powers of a matrix, assuming the determinant is a unit.
More concisely: For any square matrix `A` over a commutative ring `R` with determinant unit `det(A)`, the `(n + 1)`-th power of `A` equals the `n`-th power of `A` multiplied by `A`.
|
Matrix.Commute.zpow_right
theorem Matrix.Commute.zpow_right :
∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
{A B : Matrix n' n' R}, Commute A B → ∀ (m : ℤ), Commute A (B ^ m)
The theorem `Matrix.Commute.zpow_right` states that for any type `n'` with decidable equality and finite elements, any type `R` that is a commutative ring, and any two matrices `A` and `B` of type `Matrix n' n' R`, if `A` and `B` commute, then for any integer `m`, `A` commutes with `B` raised to the power of `m`. In other words, if the multiplication of two matrices `A` and `B` commutes (i.e., `A * B = B * A`), then the multiplication of `A` and the `m`-th power of `B` also commutes for any integer `m`.
More concisely: If matrices `A` and `B` of size `n' x n'` over a commutative ring `R` with decidable equality and finite elements commute, then `A` commutes with the power `B^m` for any integer `m`.
|
Matrix.zpow_neg_coe_nat
theorem Matrix.zpow_neg_coe_nat :
∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
(A : Matrix n' n' R) (n : ℕ), A ^ (-↑n) = (A ^ n)⁻¹
This theorem states that for any type `n'` with decidable equality and finite number of elements, and any commutative ring `R`, if `A` is a matrix with entries in `R` and indices in `n'`, and `n` is a natural number, then the negative `n`-th power of `A`, which is `A` raised to the power of `-n`, is equal to the inverse of `A` raised to the power of `n`. In mathematical terms, this can be written as: \(A^{-n} = (A^n)^{-1}\).
More concisely: For any commutative ring R, finite type n' with decidable equality, and matrix A with entries in R and indices in n', the negative n-th power of A equals the inverse of A raised to the power of n: i.e., A^(-n) = (A^n)^(-1).
|
Matrix.zpow_neg
theorem Matrix.zpow_neg :
∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
{A : Matrix n' n' R}, IsUnit A.det → ∀ (n : ℤ), A ^ (-n) = (A ^ n)⁻¹
The theorem `Matrix.zpow_neg` states that for any square matrix `A` with elements from a commutative ring `R`, where the determinant of `A` is a unit, the integer power of `A` to the negative value `-n` is the inverse of `A` to the power of `n`. Here, `n'` denotes the type used to index the rows and columns of the matrix, `n'` is assumed to have decidable equality and finite number of elements (i.e., it is a finite type). The integer `n` is the exponent in the power operation.
More concisely: For a square matrix A over a commutative ring R with determinant unit, A^(-n) = (A^n)^-1, where n is a non-zero integer and A^n is the integer power of matrix A.
|
Matrix.inv_pow'
theorem Matrix.inv_pow' :
∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
(A : Matrix n' n' R) (n : ℕ), A⁻¹ ^ n = (A ^ n)⁻¹
This theorem states that for any type `n'` with decidable equality and finite number of elements, for any commutative ring `R`, for any matrix `A` with entries in `R` and dimensions indexed by `n'`, and for any natural number `n`, the `n`th power of the inverse of `A` is the same as the inverse of the `n`th power of `A`. In mathematical notation, this would be written as $(A^{-1})^n = (A^n)^{-1}$.
More concisely: For any commutative ring R, finite type n with decidable equality, and matrix A of size n x n over R with decidable inverse, $(A^{-1})^n = (A^n)^{-1}$.
|