Moritz Doll

icon indicating a website link mcdoll.github.io

icon location Melbourne

Results 14 comments of Moritz Doll

feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology

I was thinking about something like the characterization of convergence of distributions in a `with_seminorm p` space, but as I've said the PR is long enough already.

feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology

Since there have been no further comments for a week, I think we should merge it. maintainer merge

feat(number_theory/modular_forms): Modular form definition

Sorry, I haven't followed the discussion. Almost all of my Lean attention is at mathlib4 at the moment. When I originally suggested `fun_like`, I was completely ignorant of the graded...

feat(topology,analysis): add the discrete metric and normed spaces

@eric-wieser what is the state of this PR?