Final session on Friday

Stream: LftCM22

[Heather Macbeth]

I'd love it if we could spend the final session on Friday (3:30 pm) hearing short reports on people's projects this week. Doesn't matter whether it was an "official" project or not, and doesn't matter whether you had 3 PRs to mathlib or just discovered the incomprehensibility of a part of the library.

Can we check who would be willing to give a quick report? (Virtual participants also welcome!). Unfortunately I guess some people will already have left and will be travelling then ...

[María Inés de Frutos Fernández]

@Antoine Chambert-Loir can present the progress we made on divided powers.

[Heather Macbeth]

I also have strong-armed

• @Matej Penciak for symplectic group
• @Daniel Packer for orthonormal bases
• @Jon Bannon and @Jireh Loreaux for operator algebras

More volunteers please!

[Kevin Buzzard]

@Jackie Lang and/or @Judith Ludwig can talk about their definition and construction of basic API for formally unramified and formally etale maps!

[Heather Macbeth]

We also have

• @Flo (Florent Schaffhauser) on H-spaces
• @Tyler Raven Billingsley and @Phil Wood on power series

[Jake Levinson]

@Sam van G and I can talk about the progress we made on closed embeddings of locally ringed spaces.