Trigger CI for leanprover/lean4#3078

Mathlib/Data/ZMod/Module.lean

@@ -10,25 +10,25 @@ import Mathlib.Algebra.Module.LinearMap
 # The `ZMod n`-module structure on Abelian groups whose elements have order dividing `n`
 -/
 
-variable {n : ℕ} {M M₁ : Type*} [AddCommGroup M] [AddCommGroup M₁]
-  [Module (ZMod n) M] [Module (ZMod n) M₁]
+variable {n : ℕ} {M M₁ F S : Type*} [AddCommGroup M] [AddCommGroup M₁] [AddMonoidHomClass F M M₁]
+  [Module (ZMod n) M] [Module (ZMod n) M₁] [SetLike S M] [AddSubgroupClass S M] {x : M} {K : S}
 
 namespace ZMod
 
-theorem map_smul (f : M →+ M₁) (c : ZMod n) (x : M) : f (c • x) = c • f x := by
-  cases n with
-  | zero => exact map_int_cast_smul f _ _ c x
-  | succ n =>
-    induction c using Fin.induction with
-    | zero => simp_rw [zero_smul, map_zero]
-    | succ c hc => simp_rw [← Fin.coeSucc_eq_succ, add_smul, one_smul, f.map_add, hc]
+theorem map_smul (f : F) (c : ZMod n) (x : M) : f (c • x) = c • f x := by
+  rw [← ZMod.int_cast_zmod_cast c]
+  exact map_int_cast_smul f _ _ c x
 
-end ZMod
+theorem smul_mem (hx : x ∈ K) (c : ZMod n) : c • x ∈ K := by
+  rw [← ZMod.int_cast_zmod_cast c, ← zsmul_eq_smul_cast]
+  exact zsmul_mem hx c
 
-namespace AddMonoidHom
+end ZMod
 
 variable (n)
 
+namespace AddMonoidHom
+
 /-- Reinterpret an additive homomorphism as a `ℤ/nℤ`-linear map.
 
 See also:
@@ -42,3 +42,36 @@ theorem toZModLinearMap_injective: Function.Injective <| toZModLinearMap n (M :=
 theorem coe_toZModLinearMap (f : M →+ M₁) : ⇑(f.toZModLinearMap n) = f := rfl
 
 end AddMonoidHom
+
+namespace AddSubgroup
+
+/-- Reinterpret an additive subgroup of a `ℤ/nℤ`-module as a `ℤ/nℤ`-submodule.
+
+See also: `AddSubgroup.toIntSubmodule`, `AddSubmonoid.toNatSubmodule`. -/
+def toZModSubmodule : AddSubgroup M ≃o Submodule (ZMod n) M where
+  toFun S := { S with smul_mem' := fun c _ h ↦ ZMod.smul_mem (K := S) h c }
+  invFun := Submodule.toAddSubgroup
+  left_inv _ := rfl
+  right_inv _ := rfl
+  map_rel_iff' := Iff.rfl
+
+@[simp]
+theorem toZModSubmodule_symm :
+    ⇑((toZModSubmodule n).symm : _ ≃o AddSubgroup M) = Submodule.toAddSubgroup :=
+  rfl
+
+@[simp]
+theorem coe_toZModSubmodule (S : AddSubgroup M) : (toZModSubmodule n S : Set M) = S :=
+  rfl
+
+@[simp]
+theorem toZModSubmodule_toAddSubgroup (S : AddSubgroup M) :
+    (toZModSubmodule n S).toAddSubgroup = S :=
+  rfl
+
+@[simp]
+theorem _root_.Submodule.toAddSubgroup_toZModSubmodule (S : Submodule (ZMod n) M) :
+    toZModSubmodule n S.toAddSubgroup = S :=
+  rfl
+
+end AddSubgroup

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