English
Any invertible linear map rescales Lebesgue measure by the absolute value of its determinant.
Русский
Любое обратимое линейное отображение масштабирует меру Лебега пропорционально абсолютному значению детерминанта.
LaTeX
$$$$ \\mathrm{map}(f,\\mathrm{volume}) = \\mathrm{ENNReal.ofReal}(|\\det f|^{-1}) \\cdot \\mathrm{volume}. $$$$
Lean4
/-- Any invertible linear map rescales Lebesgue measure through the absolute value of its
determinant. -/
theorem map_linearMap_volume_pi_eq_smul_volume_pi {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ} (hf : LinearMap.det f ≠ 0) :
Measure.map f volume = ENNReal.ofReal (abs (LinearMap.det f)⁻¹) • volume := by
classical
-- this is deduced from the matrix case
let M := LinearMap.toMatrix' f
have A : LinearMap.det f = det M := by simp only [M, LinearMap.det_toMatrix']
have B : f = toLin' M := by simp only [M, toLin'_toMatrix']
rw [A, B]
apply map_matrix_volume_pi_eq_smul_volume_pi
rwa [A] at hf
