Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quaternion.continuous_im_k

Modification history

2023-02-09 15:58

src/analysis/quaternion.lean

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

Added quaternion.continuous_im_k View on Github →