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 DivInvMonoid.Pow default implementation. The lemma names are taken from Algebra.GroupWithZero.Power.

Tags

matrix inverse, matrix powers

@[implicit_reducible]

noncomputable instance Matrix.instDivInvMonoid {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] : DivInvMonoid (Matrix n' n' R)

@[simp]

theorem Matrix.inv_pow' {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) (n : ℕ) : A⁻¹ ^ n = (A ^ n)⁻¹

theorem Matrix.pow_sub' {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) {m n : ℕ} (ha : IsUnit A.det) (h : n ≤ m) : A ^ (m - n) = A ^ m * (A ^ n)⁻¹

theorem Matrix.pow_inv_comm' {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) (m n : ℕ) : A⁻¹ ^ m * A ^ n = A ^ n * A⁻¹ ^ m

@[simp]

theorem Matrix.one_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (n : ℤ) : 1 ^ n = 1

theorem Matrix.zero_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (z : ℤ) : z ≠ 0 → 0 ^ z = 0

theorem Matrix.zero_zpow_eq {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (n : ℤ) : 0 ^ n = if n = 0 then 1 else 0

theorem Matrix.inv_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) (n : ℤ) : A⁻¹ ^ n = (A ^ n)⁻¹

@[simp]

theorem Matrix.zpow_neg_one {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) : A ^ (-1) = A⁻¹

@[simp]

theorem Matrix.zpow_neg_natCast {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) (n : ℕ) : A ^ (-↑n) = (A ^ n)⁻¹

theorem IsUnit.det_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (h : IsUnit A.det) (n : ℤ) : IsUnit (A ^ n).det

theorem Matrix.isUnit_det_zpow_iff {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} {z : ℤ} : IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0

theorem Matrix.zpow_neg {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (h : IsUnit A.det) (n : ℤ) : A ^ (-n) = (A ^ n)⁻¹

theorem Matrix.inv_zpow' {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (h : IsUnit A.det) (n : ℤ) : A⁻¹ ^ n = A ^ (-n)

theorem Matrix.zpow_add_one {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (h : IsUnit A.det) (n : ℤ) : A ^ (n + 1) = A ^ n * A

theorem Matrix.zpow_sub_one {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (h : IsUnit A.det) (n : ℤ) : A ^ (n - 1) = A ^ n * A⁻¹

theorem Matrix.zpow_add {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (ha : IsUnit A.det) (m n : ℤ) : A ^ (m + n) = A ^ m * A ^ n

theorem Matrix.zpow_add_of_nonpos {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} {m n : ℤ} (hm : m ≤ 0) (hn : n ≤ 0) : A ^ (m + n) = A ^ m * A ^ n

theorem Matrix.zpow_add_of_nonneg {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} {m n : ℤ} (hm : 0 ≤ m) (hn : 0 ≤ n) : A ^ (m + n) = A ^ m * A ^ n

theorem Matrix.zpow_one_add {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (h : IsUnit A.det) (i : ℤ) : A ^ (1 + i) = A * A ^ i

theorem Matrix.SemiconjBy.zpow_right {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A X Y : Matrix n' n' R} (hx : IsUnit X.det) (hy : IsUnit Y.det) (h : SemiconjBy A X Y) (m : ℤ) : SemiconjBy A (X ^ m) (Y ^ m)

theorem Matrix.Commute.zpow_right {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A B : Matrix n' n' R} (h : Commute A B) (m : ℤ) : Commute A (B ^ m)

theorem Matrix.Commute.zpow_left {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A B : Matrix n' n' R} (h : Commute A B) (m : ℤ) : Commute (A ^ m) B

theorem Matrix.Commute.zpow_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A B : Matrix n' n' R} (h : Commute A B) (m n : ℤ) : Commute (A ^ m) (B ^ n)

theorem Matrix.Commute.zpow_self {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) (n : ℤ) : Commute (A ^ n) A

theorem Matrix.Commute.self_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) (n : ℤ) : Commute A (A ^ n)

theorem Matrix.Commute.zpow_zpow_self {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) (m n : ℤ) : Commute (A ^ m) (A ^ n)

theorem Matrix.zpow_add_one_of_ne_neg_one {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (n : ℤ) : n ≠ -1 → A ^ (n + 1) = A ^ n * A

theorem Matrix.zpow_mul {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) (h : IsUnit A.det) (m n : ℤ) : A ^ (m * n) = (A ^ m) ^ n

theorem Matrix.zpow_mul' {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) (h : IsUnit A.det) (m n : ℤ) : A ^ (m * n) = (A ^ n) ^ m

@[simp]

theorem Matrix.coe_units_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (u : (Matrix n' n' R)ˣ) (n : ℤ) : ↑(u ^ n) = ↑u ^ n

theorem Matrix.zpow_ne_zero_of_isUnit_det {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] [Nonempty n'] [Nontrivial R] {A : Matrix n' n' R} (ha : IsUnit A.det) (z : ℤ) : A ^ z ≠ 0

theorem Matrix.zpow_sub {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (ha : IsUnit A.det) (z1 z2 : ℤ) : A ^ (z1 - z2) = A ^ z1 / A ^ z2

theorem Matrix.Commute.mul_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A B : Matrix n' n' R} (h : Commute A B) (i : ℤ) : (A * B) ^ i = A ^ i * B ^ i

theorem Matrix.zpow_neg_mul_zpow_self {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (n : ℤ) {A : Matrix n' n' R} (h : IsUnit A.det) : A ^ (-n) * A ^ n = 1

theorem Matrix.one_div_pow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (n : ℕ) : (1 / A) ^ n = 1 / A ^ n

theorem Matrix.one_div_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (n : ℤ) : (1 / A) ^ n = 1 / A ^ n

@[simp]

theorem Matrix.transpose_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] (A : Matrix n' n' R) (n : ℤ) : (A ^ n).transpose = A.transpose ^ n

@[simp]

theorem Matrix.conjTranspose_zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] [StarRing R] (A : Matrix n' n' R) (n : ℤ) : (A ^ n).conjTranspose = A.conjTranspose ^ n

theorem Matrix.IsSymm.zpow {n' : Type u_1} [DecidableEq n'] [Fintype n'] {R : Type u_2} [CommRing R] {A : Matrix n' n' R} (h : A.IsSymm) (k : ℤ) : (A ^ k).IsSymm