R : Type u_1
c₁ c₂ : R
⊢ (#R × R × R × R) = (#R) ^ 4
R : Type u_1
c₁ c₂ : R
⊢ (#ℍ[R,c₁,c₂]) = (#R) ^ 4
rw [mk_congr (QuaternionAlgebra.equivProd c₁ c₂)]
R : Type u_1
c₁ c₂ : R
⊢ (#R) * ((#R) * ((#R) * (#R))) = (#R) ^ 4
R : Type u_1
c₁ c₂ : R
⊢ (#R × R × R × R) = (#R) ^ 4
simp only [mk_prod, lift_id]
no goals
R : Type u_1
c₁ c₂ : R
⊢ (#R) * ((#R) * ((#R) * (#R))) = (#R) ^ 4
ring