Def Quaternion.ofComplex

Modification history

2026-02-17 23:08

Mathlib/Analysis/Quaternion.lean

chore: bump toolchain to v4.29.0-rc1 (#35459)

Deleted Quaternion.ofComplex View on Github →

2023-05-31 07:01

Mathlib/Analysis/Quaternion.lean

feat: port Analysis.Quaternion (#4515)

Added Quaternion.ofComplex View on Github →