mathlib

24f7dbdf - feat(analysis/quaternion): add `complete_space`, `module.free`, and `module.finite` instances (#18347)

feat(analysis/quaternion): add `complete_space`, `module.free`, and `module.finite` instances (#18347) The main trick here is showing that the quaternions are in isometric equivalence with 4D euclidean space.