Theorem Quaternion.coeComplex_imK

Modification history

2025-09-01 09:41

Mathlib/Analysis/Quaternion.lean

refactor: correct names of quaternion lemmas (#29190) …

Deleted Quaternion.coeComplex_imK View on Github →

2023-05-31 07:01

Mathlib/Analysis/Quaternion.lean

feat: port Analysis.Quaternion (#4515)

Added Quaternion.coeComplex_imK View on Github →