We have some declarations that can clash with Mathlib, like `Ring` and `Field`. We should either: 1. Use the definitions from Mathlib 2. Have them under our own namespaces 3. Rename them Let's discuss