Request write access

Stream: new members

[yunfei zhang]

Hi all! I’m planning to open a PR that adds some Rayleigh quotient lemmas.
Summary:
• Prove bounds for the Rayleigh quotient of a vector lying in the span of a finite subfamily of eigenvectors (unit and nonzero / non-normalized versions).
• Specialize the result to symmetric operators via LinearMap.IsSymmetric.eigenvalues and eigenvectorBasis.

Could someone with write access help review and merge the PR once it’s up (or grant the necessary write access if appropriate)?
I’m a new contributor, so any feedback on style, naming, or proof structure would be very appreciated—feel free to suggest changes, or even push a small edit / open a PR on top of mine. Thanks!

[Ruben Van de Velde]

Welcome, you no longer need any specific access to make a pull request to mathlib. Just create a fork and make a pull request as normal on github