feat(LinearAlgebra/Matrix): powers preserve IsSymm and IsHermitian (

#9036)

Mathlib/LinearAlgebra/Matrix/Hermitian.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp
 -/
 import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.LinearAlgebra.Matrix.ZPow
 
 #align_import linear_algebra.matrix.hermitian from "leanprover-community/mathlib"@"caa58cbf5bfb7f81ccbaca4e8b8ac4bc2b39cc1c"
 
@@ -215,6 +216,10 @@ theorem isHermitian_mul_mul_conjTranspose [Fintype m] {A : Matrix m m α} (B : M
   simp only [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose, hA.eq, Matrix.mul_assoc]
 #align matrix.is_hermitian_mul_mul_conj_transpose Matrix.isHermitian_mul_mul_conjTranspose
 
+lemma commute_iff [Fintype n] {A B : Matrix n n α}
+    (hA : A.IsHermitian) (hB : B.IsHermitian) : Commute A B ↔ (A * B).IsHermitian :=
+  hA.isSelfAdjoint.commute_iff hB.isSelfAdjoint
+
 end NonUnitalSemiring
 
 section Semiring
@@ -228,6 +233,9 @@ theorem isHermitian_one [DecidableEq n] : (1 : Matrix n n α).IsHermitian :=
   conjTranspose_one
 #align matrix.is_hermitian_one Matrix.isHermitian_one
 
+theorem IsHermitian.pow [Fintype n] [DecidableEq n] {A : Matrix n n α} (h : A.IsHermitian) (k : ℕ) :
+    (A ^ k).IsHermitian := IsSelfAdjoint.pow h _
+
 end Semiring
 
 section CommRing
@@ -248,6 +256,12 @@ theorem IsHermitian.adjugate [Fintype m] [DecidableEq m] {A : Matrix m m α} (hA
     A.adjugate.IsHermitian := by simp [IsHermitian, adjugate_conjTranspose, hA.eq]
 #align matrix.is_hermitian.adjugate Matrix.IsHermitian.adjugate
 
+/-- Note that `IsSelfAdjoint.zpow` does not apply to matrices as they are not a division ring. -/
+theorem IsHermitian.zpow [Fintype m] [DecidableEq m] {A : Matrix m m α} (h : A.IsHermitian)
+    (k : ℤ) :
+    (A ^ k).IsHermitian := by
+  rw [IsHermitian, conjTranspose_zpow, h]
+
 end CommRing
 
 section IsROrC

Mathlib/LinearAlgebra/Matrix/Symmetric.lean

@@ -80,6 +80,11 @@ theorem isSymm_one [DecidableEq n] [Zero α] [One α] : (1 : Matrix n n α).IsSy
   transpose_one
 #align matrix.is_symm_one Matrix.isSymm_one
 
+theorem IsSymm.pow [CommSemiring α] [Fintype n] [DecidableEq n] {A : Matrix n n α} (h : A.IsSymm)
+    (k : ℕ) :
+    (A ^ k).IsSymm := by
+  rw [IsSymm, transpose_pow, h]
+
 @[simp]
 theorem IsSymm.map {A : Matrix n n α} (h : A.IsSymm) (f : α → β) : (A.map f).IsSymm :=
   transpose_map.symm.trans (h.symm ▸ rfl)

Mathlib/LinearAlgebra/Matrix/ZPow.lean

@@ -3,8 +3,9 @@ Copyright (c) 2021 Yakov Pechersky. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
-import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
 import Mathlib.Data.Int.Bitwise
+import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
+import Mathlib.LinearAlgebra.Matrix.Symmetric
 
 #align_import linear_algebra.matrix.zpow from "leanprover-community/mathlib"@"03fda9112aa6708947da13944a19310684bfdfcb"
 
@@ -340,6 +341,10 @@ theorem conjTranspose_zpow [StarRing R] (A : M) : ∀ n : ℤ, (A ^ n)ᴴ = Aᴴ
   | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow]
 #align matrix.conj_transpose_zpow Matrix.conjTranspose_zpow
 
+theorem IsSymm.zpow {A : M} (h : A.IsSymm) (k : ℤ) :
+    (A ^ k).IsSymm := by
+  rw [IsSymm, transpose_zpow, h]
+
 end ZPow
 
 end Matrix