Mathlib Changelog
v4
Changelog
About
Github
Theorem
Quaternion.coeComplex_imJ
Modification history
2025-09-01 09:41
Mathlib/Analysis/Quaternion.lean
refactor: correct names of quaternion lemmas (#29190) …
Deleted
Quaternion.coeComplex_imJ
View on Github →
2023-05-31 07:01
Mathlib/Analysis/Quaternion.lean
feat: port Analysis.Quaternion (#4515)
Added
Quaternion.coeComplex_imJ
View on Github →