det_eq_neg_det_of_opposite_orientation

English

If bases have opposite orientation, then e.det = - f.det.

Русский

Если ориентация противоположна, то детерминант равен противоположному знаку.

LaTeX

$$$e.toBasis.det = -f.toBasis.det$ when $e.toBasis.orientation \neq f.toBasis.orientation$$$

Lean4

/-- Two orthonormal bases with opposite orientations determine opposite "determinant"
top-dimensional forms on `E`. -/
theorem det_eq_neg_det_of_opposite_orientation (h : e.toBasis.orientation ≠ f.toBasis.orientation) :
    e.toBasis.det = -f.toBasis.det :=
  by
  rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
  simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h]

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