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

[eric-wieser]

---

[loefflerd]

Wouldn't it be better to instead prove the more general result that if A and B are Hermitian and commute with each other, then A * B is Hermitian, and deduce the result for powers as a special case?

[eric-wieser]

I strongly suspect "it follows" results in a longer proof than the one I already have that just uses the existing facts about power and conjugate transpose commuting.

However, the lemma you suggest did cross my mind, and would indeed be a good result to have; I'll add the hermitian version of IsSelfAdjoint.commute_iff to this PR in a few hours.

[loefflerd]

I strongly suspect "it follows" results in a longer proof than the one I already have

I know. The suggestion wasn't intended to be taken seriously. It was intended as a demonstration of how annoying it is when people hijack a simple PR with demands for more and more tangentially-related extra functionality (as you have been doing at #8809).

[j-loreaux]

I have to say I don't love this thing of duplicating all the API for star structures. That seems silly. @eric-wieser thoughts?

[eric-wieser]

I replaced the proof for IsHermitian.pow with a call to the IsSelfAdjoint API. The zpow result is novel because the zpow operator on matrices is not captured by any existing typeclass.

[j-loreaux]

bors d+

[mathlib-bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

As discussed privately, a future refactor could consider renaming IsHermitian.zpow to IsSelfAdjoint.matrix_zpow, though such a change would amount to refactoring this entire file and so isn't really in scope for this PR.

In the meantime, we should continue to re-use IsSelfAdjoint proofs wherever possible in this file rather than reproving things.

[eric-wieser]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported