English
Volume form is invariant under composition with an orientation-preserving linear isometry.
Русский
Объемная форма сохраняется при композиции с ориентированным линейным изометрическим отображением.
LaTeX
$$$$ o.volumeForm \circ (\phi \mapsto \phi) = o.volumeForm $$$$
Lean4
/-- The volume form is invariant under pullback by a positively-oriented isometric automorphism. -/
theorem volumeForm_comp_linearIsometryEquiv (φ : E ≃ₗᵢ[ℝ] E) (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E))
(x : Fin n → E) : o.volumeForm (φ ∘ x) = o.volumeForm x :=
by
rcases n with - | n
· refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp
have : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
convert o.volumeForm_map φ (φ ∘ x)
· symm
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
rw [_i.out, Fintype.card_fin]
· ext
simp