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.
If someone wants to refactor, please go ahead.
Riccardo Brasca (Jan 26 2021 at 15:42):
I can do it. If
leanproject build succeeds it's done, right?
Johan Commelin (Jan 26 2021 at 15:43):
please do it for double complexes as well
Riccardo Brasca (Jan 26 2021 at 15:44):
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