David Kurniadi Angdinata

Thank you. It seems from reading the description above that this issue is meant to implement *imaginary* quadratic rings, as the *real* case would probably be harder to do e.g....

Right - the *discriminant* as mentioned above refers to the `d` in `Q(√d)` and not the usual term used in number theory (at least in English), so it should be...

> If you add the maximal spectrum, I think it needs to come with a lot of API about its relation to the prime spectrum: at a minimum the inclusion...

> Is the content of this PR urgent? If not, then I would prefer that you swap the order of those two PRs. I made a basic [PR for the...

@jcommelin could you tell bors to merge again?

> @sdiehl Is this library still maintained? Are you willing to pass on maintainership? I used to be its main contributor (but I should say that it is fully owned...

Since we need both univariate and bivariate division polynomials, here is my suggestion for the naming: - `φ`, `ω`, and `ψ` will be the bivariate versions defined in the usual...

I only moved the files into a subdirectory in [latest commit](https://github.com/leanprover-community/mathlib4/pull/6703/commits/7190e5e9db9dfab6883a6c4537583aec21be8441), while the changes reflecting the suggestions are in the [previous commit](https://github.com/leanprover-community/mathlib4/pull/6703/commits/fa649869b30eea69f1734b953eaf92fe64a1aaee). Note that there seems to be a weird...

Don't we need the `map` lemmas for that? I think I started #13399 pretty much immediately after I realised this. I suggest keeping the PR as it is and continue...

I think this is a massive PR, especially because it's a long argument. Can you try to split it to smaller self-contained chunks, so it's easier to review?