See page 4 of https://leanprover-community.github.io/papers/mathlib-paper.... for a part of the hierarchy of algebraic structures in the Lean theorem prover. (If you give it a normed field, it will use this hierarchy to automatically deduce that it is also a ring or a topological space, etc...)