[GOAL]
⊢ ↑LinearMap.det (AlgEquiv.toLinearMap conjAe) = -1
[PROOFSTEP]
rw [← LinearMap.det_toMatrix basisOneI, toMatrix_conjAe, Matrix.det_fin_two_of]
[GOAL]
⊢ 1 * -1 - 0 * 0 = -1
[PROOFSTEP]
simp
[GOAL]
⊢ ↑LinearEquiv.det (AlgEquiv.toLinearEquiv conjAe) = -1
[PROOFSTEP]
rw [← Units.eq_iff, LinearEquiv.coe_det, AlgEquiv.toLinearEquiv_toLinearMap, det_conjAe, Units.coe_neg_one]
