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.





leanprover-community/mathlib,leanprover-community/mathlib