English
For a basis b and a linear equivalence f, and v : ι → M', the determinant equals the determinant of the linear map composed with the inverse of f on v.
Русский
Для базиса b и линейного эквивалента f, детерминант равен детерминанту композиции с обратным отображением на v.
LaTeX
$$ (b.map f).det v = b.det (f.symm ∘ v)$$
Lean4
/-- If a basis is multiplied columnwise by scalars `w : ι → Rˣ`, then the determinant with respect
to this basis is multiplied by the product of the inverse of these scalars. -/
theorem det_unitsSMul (e : Basis ι R M) (w : ι → Rˣ) : (e.unitsSMul w).det = (↑(∏ i, w i)⁻¹ : R) • e.det :=
by
ext f
change
(Matrix.det fun i j => (e.unitsSMul w).repr (f j) i) = (↑(∏ i, w i)⁻¹ : R) • Matrix.det fun i j => e.repr (f j) i
simp only [e.repr_unitsSMul]
convert Matrix.det_mul_column (fun i => (↑(w i)⁻¹ : R)) fun i j => e.repr (f j) i
simp [← Finset.prod_inv_distrib]
