Q' SES

Stream: condensed mathematics

[Adam Topaz]

I have a working skeleton for the Q' SES. But there was a missing assumption in pseudo_normed_group/QprimeFP.lean, so some things may break once I push. Please bear with me for a little while as I add this necessary assumption in other places!

[Johan Commelin]

What was the missing assumption?

[Adam Topaz]

For all naturals $m$ and all $r \in \mathbb{R}_{\geq 0}$ there exists some natural $n$ such that $r \le \kappa \ (\iota n) \ m$

[Johan Commelin]

Aha! Good catch (-;

[Adam Topaz]

Okay, only props are left now in QprimeFP

[Adam Topaz]

I got annoyed and just sorried the missing hypotheses inside a proof, so that will have to be fixed at some point

[Johan Commelin]

I'm a bit busy with ICERM right now, but I hope to take a look later today.

[Adam Topaz]

Is challenge the only file that depends on Lbar/ext?

[Adam Topaz]

BTW it took some crazy gymnastics with various isomorphisms in QprimeFP to reduce the SES to the stuff from bd_ses.lean, so some of the sorries there might be challenging