Double quotients for algebras

Stream: new members

[Peiran Wu]

Hello! I'm not technically a new member as I've been here since 2017, when I was at Imperial, but I've not done much Lean since and never introduced myself here. Now I'm a PhD student at St Andrews (UK) working on finite permutation groups. I'm preparing for my first PR, generalising definitions and lemmas on double quotients from rings to algebras. This is a easy topic to get myself started, suggested to me by @David Ang. Could someone invite me to the mathlib repo on GtiHub? My handle is "wupr".

[Riccardo Brasca]

Welcome back! You should have received an invitation.

[Peiran Wu]

Thank you!

[Kevin Buzzard]

Hi Peiran! Nice to see you here! I'm speaking at St Andrews in a couple of weeks BTW.

[Peiran Wu]

Hi Kevin! Yes, I saw your talk on this semester's schedule. I can't wait.

[Paul Lezeau]

@Peiran Wu Feel free to ping me for a review once your code is ready ;)

[Paul Lezeau]

(I'm the "Eric!" you chatted with on the Xena server)

[David Ang]

@Paul Lezeau #18452

[Paul Lezeau]

Noted !