mathlib PR

Stream: new members

[Bernd Losert]

I made a PR to mathlib (https://github.com/leanprover-community/mathlib/pull/11445), but the PR is in a fork. I was told that I should make a branch instead, but I can't push the branch without the required permission. Can someone grant me the required permissions please?

My github username is berndlosert.

[Patrick Massot]

Done. Sorry I should have checked whether you were already in.

[Bernd Losert]

Thanks!