write access request

Stream: mathlib4

[Jou Glasheen]

Hi,

Could you please grant me (jouglasheen) write access to non-master branches of the mathlib repository?

I am a master's student at Imperial, supervised by @Kevin Buzzard . I am working on admissible representations of p-adic reductive groups. I would like to contribute a proof that nonarchimedean groups are totally disconnected, and proofs of the padic integers being totally disconnected and compact.

[Markus Himmel]

@Jou Glasheen done: https://github.com/leanprover-community/mathlib4/invitations

[Yakov Pechersky]

Totally disconnected is in a PR #14768: https://github.com/leanprover-community/mathlib4/blob/pechersky%2Fultrametric-space-normed/Mathlib%2FTopology%2FMetricSpace%2FUltra%2FTotallyDisconnected.lean

[Yakov Pechersky]

Although your proof might not go through metric spaces

[Jou Glasheen]

Yakov Pechersky said:

Totally disconnected is in a PR #14768: https://github.com/leanprover-community/mathlib4/blob/pechersky%2Fultrametric-space-normed/Mathlib%2FTopology%2FMetricSpace%2FUltra%2FTotallyDisconnected.lean

Sorry -- I wrote the wrong thing : I meant that I have Z_[p] is totally bounded. I will also have that Q_[p] is locally compact, soon.