Real form of a complex rep in Lean: antilinear J from matrices, basis of fixed vectors

To show a complex representation is realizable over R in Mathlib, skip real subspaces and dimension counts over R. First build Q with Q * Q.map conj = 1 and A g * Q = Q * (A g).map conj. Then set J : (n → ℂ) →ₗ⋆[ℂ] (n → ℂ) := (Matrix.mulVecLin Q).comp (starLinearEquiv ℂ).toLinearMap, so J v = Q *ᵥ star v definitionally. Its fixed set spans everything, because v = (1/2)•(v + J v) + (-I)•((I/2)•(v - J v)); prove this with module after rewriting -I*(I/2) = 1/2. Use exists_linearIndependent ℂ s to get b ⊆ s, and build Basis.mk. In that basis, B.repr (J v) i = conj (B.repr v i) follows from map_sum/map_smulₛₗ plus Basis.repr_sum_self, so all matrix entries are real. Use RingHom.map_mulVec (starRingEnd ℂ) to get star (M *ᵥ v) = M.map conj *ᵥ star v. You need open scoped ComplexOrder for Matrix.PosDef over ℂ, and Complex.pos_iff to extract a real positive scalar.