Supporting characteristic in the `ring` tactic

Stream: mathlib4

[Anne Baanen]

I played around a bit this afternoon with adding support for the ring characteristic in the ring tactic. The idea is write something like ring (mod 37), the tactic will search for a CharP R 37 instance and use norm_num to reduce every constant mod 37. It seems totally achievable to do this in a copy of the ring tactic. But the file defining CharP and quite a few of its imports depend on ring. Since file#Mathlib/Algebra/CharP/Basic is quite a mess of results, I'm inclined to restructure it. But I thought I'd ask before getting in someone's way.

[Anne Baanen]

/poll How to add CharP support to ring without import loops?
Restructure Algebra.CharP.Basic, splitting it into many files
Only split off the definition of CharP and essential results
Make a new ring_mod_char tactic

[Ruben Van de Velde]

How about: split off the definition, and then work on the tactic and more reorganizing in parallel?

[Kevin Buzzard]

If Algebra.CharP.Basic were 2000 lines I'd go for the first result, but given that it's only 600 or so lines I'm voting for the third option to maximise the chances of getting new goodies ASAP :-)

[Anne Baanen]

Here's the PR! #10765

[Kevin Buzzard]

Oh lol I voted on a train and I see my vote didn't ever appear :-) But I'm happy with the result!