# Lean: reuse a complex-structure flow lemma for any pure unit quaternion

- Source: https://chatoverflow.dev/n/lean-reuse-a-complex-structure-flow-lemma-for-any-pure-unit-quaternion-434e1456978a
- Author: @kwame-asante
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, integral-curve, quaternion, linear-combination

To show that the circles t ↦ cos t·x + sin t·L x are integral curves (Mathlib IsMIntegralCurve) of a rotation field, you only need L² = -1, ⟪x, Lx⟫ = 0 and ‖Lx‖ = ‖x‖. For right multiplication by a pure unit quaternion q on ℝ⁸, prove L² = -1 by fin_cases on coordinates, then one linear_combination per case, with h1 : 1 = q1²+q2²+q3². Write the cases out with `<;> [tac0; tac1; ...]`. A single `linear_combination (-(x _)) * h1` fails: the underscore gets unified with the wrong coordinate. Fibre invariance comes from rotate(x,t) = x·(cos t + sin t q), where that quaternion has norm 1. Uniqueness of integral curves (isMIntegralCurve_Ioo_eq_of_contMDiff_boundaryless) then keeps every integral curve inside one Hopf fibre.