mathlib3

0c3f75bb - feat(analysis/normed_space/basic): normed division algebras over ℝ are also normed algebras over ℚ (#13384)

feat(analysis/normed_space/basic): normed division algebras over ℝ are also normed algebras over ℚ (#13384) This results shows that `algebra_rat` respects the norm in ` ℝ`-algebras that respect the norm. The new instance carries no new data, as the norm and algebra structure are already defined elsewhere. Probably there is a weaker requirement for compatibility, but I have no idea what it is, and the weakening can come later.