Alex J Best

Looks like one way of getting this feature working is to ensure that the following jupyterlab extension is installed: https://github.com/jupyterlab/jupyter-renderers/tree/master/packages/mathjax3-extension you can do this with `jupyter labextension install @jupyterlab/mathjax3-extension` when...

Ideally Hecke should be able to check that mathjax 3 is available somehow, it already detects that ijulia is loaded and otherwise doesn't use the toggle feature, I imagine it's...

I think we might want a multiplicative group version of this too? with the one here generated by to_additive? Certainly there are nice examples like algebraically closed fields that are...

I also think this notion could be more useful when defined for `comm_monoid`s, so we cover groups_with_zero too, (such as fields again), the property of nat divisibility implies int divisibility...

> > I think we might want a multiplicative group version of this too? with the one here generated by to_additive? Certainly there are nice examples like algebraically closed fields...

This PR really makes me wonder if the rest of the file can be simplified a bit! But that's a question for another PR I guess

Yes, the rationals are a Archimedean field that is linearly ordered but is not the reals

Bhavik's work is at [irrational-pi](https://github.com/leanprover-community/mathlib/blob/irrational-pi/src/analysis/special_functions/trigonometric/pi.lean)

Sorry I should have been more clear, the two large files in measure theory are from https://github.com/jtristan/stump-learnable if the authors are ok with it I will PR the relevant parts...

> Should this depend on #8695 instead of #8642 ? Because it seems that the former supersedes the latter. It should, thanks @jcommelin somehow I missed #8695 (thanks @PatrickMassot !!)