det_to_matrix_orthonormalBasis_of_same_orientation

English

The change-of-basis matrix between two orthonormal bases with the same orientation has determinant 1.

Русский

Матрица перехода между двумя ортонормированными базисами с той же ориентацией имеет детерминант 1.

LaTeX

$$$e.toBasis.det f = 1$ when $e.toBasis.orientation = f.toBasis.orientation$$$

Lean4

/-- The change-of-basis matrix between two orthonormal bases with the same orientation has
determinant 1. -/
theorem det_to_matrix_orthonormalBasis_of_same_orientation (h : e.toBasis.orientation = f.toBasis.orientation) :
    e.toBasis.det f = 1 := by
  apply (e.det_to_matrix_orthonormalBasis_real f).resolve_right
  have : 0 < e.toBasis.det f := by
    rw [e.toBasis.orientation_eq_iff_det_pos] at h
    simpa using h
  linarith

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