mathlib documentation

linear_algebra.matrix.fpow

Integer powers of square matrices #

In this file, we define integer power of matrices, relying on the nonsingular inverse definition for negative powers.

Implementation details #

The main definition is a direct recursive call on the integer inductive type, as provided by the div_inv_monoid.gpow default implementation. The lemma names are taken from algebra.group_with_zero.power.

Tags #

matrix inverse, matrix powers

@[instance]
def matrix.div_inv_monoid {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] :
Equations
@[simp]
theorem matrix.inv_pow' {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (n : ) :
A⁻¹ ^ n = (A ^ n)⁻¹
theorem matrix.pow_sub' {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) {m n : } (ha : is_unit A.det) (h : n m) :
A ^ (m - n) = A ^ m (A ^ n)⁻¹
theorem matrix.pow_inv_comm' {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (m n : ) :
A⁻¹ ^ m A ^ n = A ^ n A⁻¹ ^ m
@[simp]
theorem matrix.one_fpow {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (n : ) :
1 ^ n = 1
theorem matrix.zero_fpow {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (z : ) :
z 00 ^ z = 0
theorem matrix.zero_fpow_eq {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (n : ) :
0 ^ n = ite (n = 0) 1 0
theorem matrix.inv_fpow {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (n : ) :
A⁻¹ ^ n = (A ^ n)⁻¹
@[simp]
theorem matrix.fpow_neg_one {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) :
A ^ -1 = A⁻¹
theorem matrix.fpow_coe_nat {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (n : ) :
A ^ n = A ^ n
@[simp]
theorem matrix.fpow_neg_coe_nat {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (n : ) :
A ^ -n = (A ^ n)⁻¹
theorem is_unit.det_fpow {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (h : is_unit A.det) (n : ) :
is_unit (A ^ n).det
theorem matrix.is_unit_det_fpow_iff {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} {z : } :
is_unit (A ^ z).det is_unit A.det z = 0
theorem matrix.fpow_neg {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (h : is_unit A.det) (n : ) :
A ^ -n = (A ^ n)⁻¹
theorem matrix.inv_fpow' {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (h : is_unit A.det) (n : ) :
A⁻¹ ^ n = A ^ -n
theorem matrix.fpow_add_one {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (h : is_unit A.det) (n : ) :
A ^ (n + 1) = (A ^ n) * A
theorem matrix.fpow_sub_one {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (h : is_unit A.det) (n : ) :
A ^ (n - 1) = (A ^ n) * A⁻¹
theorem matrix.fpow_add {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (ha : is_unit A.det) (m n : ) :
A ^ (m + n) = (A ^ m) * A ^ n
theorem matrix.fpow_add_of_nonpos {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} {m n : } (hm : m 0) (hn : n 0) :
A ^ (m + n) = (A ^ m) * A ^ n
theorem matrix.fpow_add_of_nonneg {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} {m n : } (hm : 0 m) (hn : 0 n) :
A ^ (m + n) = (A ^ m) * A ^ n
theorem matrix.fpow_one_add {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (h : is_unit A.det) (i : ) :
A ^ (1 + i) = A * A ^ i
theorem matrix.semiconj_by.fpow_right {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A X Y : matrix n' n' R} (hx : is_unit X.det) (hy : is_unit Y.det) (h : semiconj_by A X Y) (m : ) :
semiconj_by A (X ^ m) (Y ^ m)
theorem matrix.commute.fpow_right {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A B : matrix n' n' R} (h : commute A B) (m : ) :
commute A (B ^ m)
theorem matrix.commute.fpow_left {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A B : matrix n' n' R} (h : commute A B) (m : ) :
commute (A ^ m) B
theorem matrix.commute.fpow_fpow {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A B : matrix n' n' R} (h : commute A B) (m n : ) :
commute (A ^ m) (B ^ n)
theorem matrix.commute.fpow_self {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (n : ) :
commute (A ^ n) A
theorem matrix.commute.self_fpow {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (n : ) :
commute A (A ^ n)
theorem matrix.commute.fpow_fpow_self {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (m n : ) :
commute (A ^ m) (A ^ n)
theorem matrix.fpow_bit0 {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (n : ) :
A ^ bit0 n = (A ^ n) * A ^ n
theorem matrix.fpow_add_one_of_ne_neg_one {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (n : ) :
n -1A ^ (n + 1) = (A ^ n) * A
theorem matrix.fpow_bit1 {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (n : ) :
A ^ bit1 n = ((A ^ n) * A ^ n) * A
theorem matrix.fpow_mul {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (h : is_unit A.det) (m n : ) :
A ^ m * n = (A ^ m) ^ n
theorem matrix.fpow_mul' {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (h : is_unit A.det) (m n : ) :
A ^ m * n = (A ^ n) ^ m
@[simp]
theorem matrix.units.coe_inv'' {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (u : units (matrix n' n' R)) :
@[simp]
theorem matrix.units.coe_fpow {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (u : units (matrix n' n' R)) (n : ) :
(u ^ n) = u ^ n
theorem matrix.fpow_ne_zero_of_is_unit_det {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] [nonempty n'] [nontrivial R] {A : matrix n' n' R} (ha : is_unit A.det) (z : ) :
A ^ z 0
theorem matrix.fpow_sub {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (ha : is_unit A.det) (z1 z2 : ) :
A ^ (z1 - z2) = A ^ z1 / A ^ z2
theorem matrix.commute.mul_fpow {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A B : matrix n' n' R} (h : commute A B) (i : ) :
(A * B) ^ i = (A ^ i) * B ^ i
theorem matrix.fpow_bit0' {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (n : ) :
A ^ bit0 n = (A * A) ^ n
theorem matrix.fpow_bit1' {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (A : matrix n' n' R) (n : ) :
A ^ bit1 n = ((A * A) ^ n) * A
theorem matrix.fpow_neg_mul_fpow_self {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] (n : ) {A : matrix n' n' R} (h : is_unit A.det) :
(A ^ -n) * A ^ n = 1
theorem matrix.one_div_pow {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (n : ) :
(1 / A) ^ n = 1 / A ^ n
theorem matrix.one_div_fpow {n' : Type u_1} [decidable_eq n'] [fintype n'] {R : Type u_2} [comm_ring R] {A : matrix n' n' R} (n : ) :
(1 / A) ^ n = 1 / A ^ n