Mathlib v3 is deprecated. Go to Mathlib v4

Theorem quaternion.norm_coe

Modification history

2022-11-17 13:13
src/analysis/quaternion.lean
refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …
Modified quaternion.norm_coeView on Github →
2020-11-04 05:43
src/analysis/quaternion.lean
feat(data/quaternion): define quaternions and prove some basic properties (#2339)
Added quaternion.norm_coeView on Github →