## Stream: condensed mathematics

#### Johan Commelin (Jan 26 2021 at 15:39):

We should change the definition of admissible from bound_by f 1 to \forall x, \|f x\| \le x. The latter inequality is what we want to use in practice.

#### Riccardo Brasca (Jan 26 2021 at 15:42):

I can do it. Ifleanproject build succeeds it's done, right?

#### Johan Commelin (Jan 26 2021 at 15:43):

please do it for double complexes as well

OK

#### Riccardo Brasca (Jan 26 2021 at 16:10):

It's done... it was used only in the snake lemma, to that was really fast

Last updated: May 09 2021 at 22:13 UTC