Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(LinearAlgebra/Matrix): powers preserve IsSymm and IsHermitian #9036

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(LinearAlgebra/Matrix): powers preserve IsSymm and IsHermitian #9036

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
645c094
feat(LinearAlgebra/Matrix): powers preserve `IsSymm` and `IsHermitian`
eric-wieser Dec 13, 2023
1858ef4
add commute_iff for good measure
eric-wieser Dec 14, 2023
4a661bb
deduplicate a little
eric-wieser Dec 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions Mathlib/LinearAlgebra/Matrix/Hermitian.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
5 changes: 5 additions & 0 deletions Mathlib/LinearAlgebra/Matrix/Symmetric.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
7 changes: 6 additions & 1 deletion Mathlib/LinearAlgebra/Matrix/ZPow.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand Down Expand Up @@ -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
Loading