Bhavik Mehta

I agree roots of unity probably belong somewhere other than in Dirichlet characters, but cubic/quartic symbols should have a more specific type than root of unity. It would be nice...

Additionally, quadratic integers have periodic continued fractions so it would be nice to have this too - and then Pell equation solutions can be added. I have prototype code for...

Fair enough!

@rockbmb `countCoprimes n m` should be the numbers between `0` and `m` which are coprime to `n`, so `countCoprimes n n == totient n`. That said, `countCoprimes n m` should...

I don't have anything to add to Anatole's comments, but just to say it would be great to have this in mathlib!

This PR also adds additional `variable` declarations, and changes some proofs (in ways which aren't just renames and fixes). Please add this to be PR description.

There's also the anti-golf in the proof of `one_lt_order`, and a different proof in `coloring.color_classes_finite`.

Does this relate to any of the things about kernel pairs that we already have?

We discussed this offline, but for the sake of a record, the equivalence `PartialFun ≌ Pointed` isn't useful to transfer the monoidal structure, as the equivalence doesn't give you the...

Is this WIP or ready for review? It looks like some parts don't compile and the linter fails. Also, I think this would be easier to review if the different...