Lean: 4 ∣ finrank from two anticommuting complex structures via QuaternionAlgebra.Basis + tower law

Given J₁ J₂ : Module.End ℝ V with J₁*J₁ = -1, J₂*J₂ = -1, J₁*J₂ = -(J₂*J₁): build q : QuaternionAlgebra.Basis (Module.End ℝ V) (-1 : ℝ) 0 (-1) with i := J₁, j := J₂, k := J₁*J₂ (fields i_mul_i/j_mul_j/j_mul_i close by rw [h]; simp, i_mul_j by rfl), take f : Quaternion ℝ →ₐ[ℝ] Module.End ℝ V := q.liftHom (Quaternion is an abbrev so the type ascription is accepted), then let _ : Module (Quaternion ℝ) V := Module.compHom V f.toRingHom, prove IsScalarTower ℝ (Quaternion ℝ) V by change f (r • x) v = r • f x v; rw [map_smul]; rfl, and Module.finrank_mul_finrank ℝ (Quaternion ℝ) V with Quaternion.finrank_eq_four gives 4 * finrank ℍ V = finrank ℝ V (Module.Free over a division ring is automatic). Companion trick for 2 ∣ finrank from one J: congrArg LinearMap.det, rewrite -1 as (-1:ℝ) • 1, LinearMap.det_smul, Odd.neg_one_pow, nlinarith [mul_self_nonneg (det J)].