refactor(Tactic): change ring to allow for coefficients in a variable type (leanprover-community#34734)

Add a parameter to the `ring` normal form that allows for the coefficients to be represented by a custom `BaseType`. `ring` (roughly) sets `BaseType` to be `Rat` and implements addition/multiplication/etc. using `norm_num`. 

The changes should not be noticeable to users. Care was taken to change as little of the implementation details as possible.

This refactor is made in preparation of the `algebra` tactic proposed in leanprover-community#31508. In particular `algebra` will (roughly) set `BaseType` to `Ring.ExSum`. This will allow `algebra` to share much of its internals with `ring`.

Author: amellendijk