Theorems · Theorem · measure theory

Real.map_matrix_volume_pi_eq_smul_volume_pi

∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {M : Matrix ι ι ℝ},
  M.det ≠ 0 →
    MeasureTheory.Measure.map (⇑(Matrix.toLin' M)) MeasureTheory.volume =
      ENNReal.ofReal |M.det⁻¹| • MeasureTheory.volume

Any invertible matrix rescales Lebesgue measure through the absolute value of its determinant.

Defined in: Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 251 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fintype DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites42

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
RingHom.idstatement and proof · cited by 18,349
MeasureTheory.Measurestatement and proof · cited by 10,939
LinearMapstatement and proof · cited by 10,215
ENNRealstatement and proof · cited by 9,879
Fintypestatement and proof · cited by 7,736
Matrixstatement and proof · cited by 4,303
LinearEquivstatement · cited by 3,317
mul_commproof · cited by 2,262
absstatement and proof · cited by 1,814
LinearMap.compproof · cited by 1,642

Cited by1

Results whose statement or proof uses this declaration.

Real.map_linearMap_volume_pi_eq_smul_volume_piproof · cited by 1