no goals
R : Type u_2
A : Type u_1
B : Type ?u.31470
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
c₁ c₂ : R
q : Basis A c₁ c₂
⊢ q.j * q.k = -c₂ • q.i
rw [← i_mul_j, ← mul_assoc, j_mul_i, neg_mul, k_mul_j, neg_smul]