refactor: make charP_to_charZero an instance

[ChrisHughes24]

---

This should be safe now that instance cycles are allowed in Lean4

[kbuzzard]

I've seen those build errors before, when changing unrelated files. Typeclass inference spends a long time doing a stupid thing (it's ring1 failing to prove F[X][X] has char 0), and random changes can push it over the edge. Either increase the numbers or disable the instance which is causing all the problems (it's StrictOrderedSemiring.to_charZero, you can attribute [-instance] it)

[ChrisHughes24]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5629904.
There were significant changes against commit 8712fab:

  Benchmark                             Metric           Change
  =============================================================
- build                                 native linking    11.1%
- ~Mathlib.NumberTheory.SumTwoSquares   instructions       5.8%

[ocfnash]

Empirically typeclass cycles are still bad, at least in my experience. I recently tried to promote two theorems to instances and ran into non-trivial problems (to say nothing of performance hits). I mentioned this here:
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/type.20class.20inference.20looping/near/385635549

IMHO, the situation is better than Lean 3 but I think typeclass inference still has a lot of room for improvement in Lean 4 (which is actually pretty exciting, as I believe we'll see it happen).

So unfortunately I think we should not make this change.

[ocfnash]

I'd like to have this but I think Mathlib / Lean is not yet ready.

[ocfnash]

In addition to the disappointing benchmark results I think this is a pretty big red flag.

[ocfnash]

I just came across this PR again (tidying my notifications) and it occurs to me that the right fix would be to change the definition of the CharP class to the mathematically more sensible:

class CharP [AddMonoidWithOne R] (p : ℕ) : Prop where
  cast_eq_iff' : ∀ x y : ℕ, (x : R) = (y : R) ↔ (x : ZMod p) = (y : ZMod p)

and then delete CharZero since it is then equivalent (even without additive inverses) to CharP R 0.

For bonus points one could even rename CharP to Char!