English
The absolute value of the volume form evaluated at a given vector is the same as the absolute value of the determinant in a basis; i.e., |volumeForm(v)| = |basis.det(v)| for an appropriate basis.
Русский
Модуль значения объемной формы, применяемой к векторам, совпадает с модулем детерминанта в базисе; то есть |volumeForm(v)| = |det(v)| для соответствующего базиса.
LaTeX
$$$$ |o.volumeForm(v)| = |b.toBasis.det(v)| \quad\text{for } b \text{ with orientation } b.toBasis.orientation = o. $$$$
Lean4
theorem volumeForm_robust' (b : OrthonormalBasis (Fin n) ℝ E) (v : Fin n → E) : |o.volumeForm v| = |b.toBasis.det v| :=
by
cases n
· refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp
·
rw [o.volumeForm_robust (b.adjustToOrientation o) (b.orientation_adjustToOrientation o),
b.abs_det_adjustToOrientation]
