From 05d5e25997729e6dc50432350a6e8210b0d65031 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 15 Dec 2023 23:57:43 +0000
Subject: [PATCH] feat(LinearAlgebra/Matrix): powers preserve `IsSymm` and
 `IsHermitian` (#9036)

---
 Mathlib/LinearAlgebra/Matrix/Hermitian.lean | 14 ++++++++++++++
 Mathlib/LinearAlgebra/Matrix/Symmetric.lean |  5 +++++
 Mathlib/LinearAlgebra/Matrix/ZPow.lean      |  7 ++++++-
 3 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/Mathlib/LinearAlgebra/Matrix/Hermitian.lean b/Mathlib/LinearAlgebra/Matrix/Hermitian.lean
index 009282fee170cc..25b5cb610bd7eb 100644
--- a/Mathlib/LinearAlgebra/Matrix/Hermitian.lean
+++ b/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
diff --git a/Mathlib/LinearAlgebra/Matrix/Symmetric.lean b/Mathlib/LinearAlgebra/Matrix/Symmetric.lean
index 4cf0875e0dda98..14f6f68ee388bb 100644
--- a/Mathlib/LinearAlgebra/Matrix/Symmetric.lean
+++ b/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)
diff --git a/Mathlib/LinearAlgebra/Matrix/ZPow.lean b/Mathlib/LinearAlgebra/Matrix/ZPow.lean
index a1f2b1c120c6a3..680cb6df6ce604 100644
--- a/Mathlib/LinearAlgebra/Matrix/ZPow.lean
+++ b/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