no goals
R : Type u_2
A : Type u_1
B : Type ?u.24590
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.k * q.i = -c₁ • q.j
rw [← i_mul_j, mul_assoc, j_mul_i, mul_neg, i_mul_k, neg_smul]