mathlib

mathlib copied to clipboard

This proof felt a bit painful - I suspect most of the results I needed already exist somewhere else.

This decomposition instances inherits the noncomputability of orthogonal_projection, but it is at least defeq to something useful.

---

If I understand correctly, the mathematical point here is to establish the formula orthogonal_projection (V i) x for the i-th component of (the symm of) the direct sum decomposition. Perhaps the structure of the proof would become clearer if you stated it in this way?

At a guess, the problem could be that we're missing finitary n-ary versions of lemmas which currently exist in a 2-ary form for pairs of subspaces.

I've added the missing helper lemmas to make this result a bit easier.

This PR/issue depends on:

• ~~leanprover-community/mathlib#18705~~ By Dependent Issues (🤖). Happy coding!

bors d+

:v: 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.

bors merge

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

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