det_adjustToOrientation — Mathlib

English

The determinant after adjustToOrientation has the same absolute value as before.

Русский

По абсолютному значению детерминант не изменяется после adjustToOrientation.

LaTeX

$$$\big| (e.adjustToOrientation x).toBasis.det v \big| = \big| e.toBasis.det v \big|$$$

Lean4

theorem det_adjustToOrientation :
    (e.adjustToOrientation x).toBasis.det = e.toBasis.det ∨ (e.adjustToOrientation x).toBasis.det = -e.toBasis.det := by
  simpa using e.toBasis.det_adjustToOrientation x

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