same_orientation_iff_det_eq_det — Mathlib

English

Two orthonormal bases have the same orientation iff their determinants are equal.

Русский

Два ортонормированных базиса имеют одинаковую ориентацию тогда и только тогда, когда их детерминанты равны.

LaTeX

$$$e.toBasis.det = f.toBasis.det \Leftrightarrow e.toBasis.orientation = f.toBasis.orientation$$$

Lean4

/-- Two orthonormal bases with the same orientation determine the same "determinant" top-dimensional
form on `E`, and conversely. -/
theorem same_orientation_iff_det_eq_det :
    e.toBasis.det = f.toBasis.det ↔ e.toBasis.orientation = f.toBasis.orientation :=
  by
  constructor
  · intro h
    dsimp [Basis.orientation]
    congr
  · intro h
    rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
    simp [e.det_to_matrix_orthonormalBasis_of_same_orientation f h]

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