abs_det_adjustToOrientation — Mathlib

English

The absolute values of the determinants coincide after adjusting orientation.

Русский

Кратное модулю детерминанта сохраняется после изменения ориентации.

LaTeX

$$$$ |(e.{\\rm adjustToOrientation} x).{\\rm det} v| = |e.{\\rm det} v| $$$$

Lean4

@[simp]
theorem abs_det_adjustToOrientation [Nonempty ι] (e : Basis ι R M) (x : Orientation R M ι) (v : ι → M) :
    |(e.adjustToOrientation x).det v| = |e.det v| := by rcases e.det_adjustToOrientation x with h | h <;> simp [h]

Похожие утверждения