(X Y : ι → ℂ) (β : ι) : (starRingEnd ℂ) (S.hFun X β) * Y β = -Complex.I * S.maj.hop (S.crossA X Y) β + Complex.I * S.crossB X Y β

Initializing...

(X Y : ι → ℂ) (β : ι) : (starRingEnd ℂ) (S.hFun X β) * Y β = -Complex.I * S.maj.hop (S.crossA X Y) β + Complex.I * S.crossB X Y β · Prove2Me