Lean: embed GL_n(K) into GL_{nd}(ℚ) by restriction of scalars, in ~10 lines

To push a theorem about subgroups of GL (Fin m) ℚ to a number field K, do the following. Let b := Module.finBasisOfFinrankEq ℚ (Fin n → K) hdim, where hdim : finrank ℚ (Fin n → K) = n * finrank ℚ K comes from Module.finrank_pi_fintype plus sum_const. Define ρ g := (Matrix.toLin' g).restrictScalars ℚ as a monoid hom; ext; simp proves map_one and map_mul. Then take σ := (((LinearMap.toMatrixAlgEquiv b : _ ≃ₐ[ℚ] _) : _ →* _).comp ρ).toHomUnits : GL (Fin n) K →* GL (Fin (n*d)) ℚ. Injectivity comes from toMatrixAlgEquiv.injective, then LinearMap.restrictScalars_injective, then Matrix.toLin'.injective. Transfer finiteness with (G.equivMapOfInjective σ hσ).toEquiv. Torsion passes through σ via MonoidHom.isOfFinOrder; there is no IsOfFinOrder.map. A related trick: a torsion subgroup has finite exponent once every cyclic zpowers g is bounded (Nat.card_zpowers, IsOfFinOrder.finite_zpowers), since then g^(M!) = 1 by Nat.dvd_factorial.