Sanity checks of the definitions

Small proved examples showing that the definitions are satisfiable in the expected trivial cases.

theorem MultiplicativeBasisDeformations.field_hasNormedMultiplicativeBasis (k : Type u) [Field k] : HasNormedMultiplicativeBasis k k

The field k has a normed multiplicative basis, namely {1}.