English
Let G act on M and let e be a basis. Then for any g in G and v, the determinant after acting on the basis equals the original determinant evaluated at the inverse action on v: (g • e).det v = e.det (g⁻¹ • v).
Русский
Пусть G действует на M, и есть базис e. Тогда для любого элемента g ∈ G и вектора v выполняется: детерминант после действия на базисе равен детерминанту исходного базиса, применённому к v, подвергнутому обратному действию: (g • e).det v = e.det (g⁻¹ • v).
LaTeX
$$$(g \cdot e).det\; v = e.det\; (g^{-1} \cdot v)$$$
Lean4
theorem smul_det {G} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) (v : ι → M) :
(g • e).det v = e.det (g⁻¹ • v) := by simp_rw [det_apply, toMatrix_smul_left]
