mathlib

mathlib copied to clipboard

Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/adding.20angles

---

• [x] depends on: #16475
• [x] depends on: #16476
• [x] depends on: #16477
• [x] depends on: #16478
• [x] depends on: #16479
• [x] depends on: #16487
• [x] depends on: #16928
• [ ] depends on: #16929
• [ ] depends on: #16939

This PR/issue depends on:

• ~~leanprover-community/mathlib#16475~~
• ~~leanprover-community/mathlib#16476~~
• ~~leanprover-community/mathlib#16477~~
• ~~leanprover-community/mathlib#16478~~
• ~~leanprover-community/mathlib#16479~~
• ~~leanprover-community/mathlib#16487~~
• ~~leanprover-community/mathlib#16928~~
• ~~leanprover-community/mathlib#16929~~
• ~~leanprover-community/mathlib#16939~~ By Dependent Issues (🤖). Happy coding!

I think my previous comment (that lemmas should be added that can be used to provide (hf : (orientation.map (fin 2) f.to_linear_equiv o) = complex.orientation), for lemmas with such a hypothesis, for orientations related to an orthonormal basis and an isometry given by complex.isometry_of_orthonormal, along with similar lemmas about mapping in the other direction) still applies, unless I've missed such lemmas being added somewhere - GitHub is hiding that comment by default, but only because there are so many commits in this PR, not because it's been resolved. As far as I can tell, the two_dim file has three lemmas with such a hypothesis, but no lemmas to fill such a hypothesis.

I think my previous comment (that lemmas should be added that can be used to provide (hf : (orientation.map (fin 2) f.to_linear_equiv o) = complex.orientation), for lemmas with such a hypothesis, for orientations related to an orthonormal basis and an isometry given by complex.isometry_of_orthonormal, along with similar lemmas about mapping in the other direction) still applies, unless I've missed such lemmas being added somewhere - GitHub is hiding that comment by default, but only because there are so many commits in this PR, not because it's been resolved. As far as I can tell, the two_dim file has three lemmas with such a hypothesis, but no lemmas to fill such a hypothesis.

I completely agree with this remark (and the similar remarks made in the comment above). However, there are already so many lines changing here that I think it is better to defer this to a follow-up PR.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests