orientation_comp_linearEquiv_eq_neg_iff_det_neg

English

The orientation after composing with a linear equivalence is the negation of the original orientation if and only if the determinant of the equivalence is negative.

Русский

Ориентация после композиции с линейной эквивалентностью является отрицанием исходной ориентации тогда и только тогда, когдаdet эквивалентности отрицателен.

LaTeX

$$$$ (e.map f).{\\rm orientation} = -e.{\\rm orientation} \\iff \\det f < 0 $$$$

Lean4

/-- Composing a basis with a linear equiv gives the negation of that orientation if and only if
the determinant is negative. -/
theorem orientation_comp_linearEquiv_eq_neg_iff_det_neg (e : Basis ι R M) (f : M ≃ₗ[R] M) :
    (e.map f).orientation = -e.orientation ↔ LinearMap.det (f : M →ₗ[R] M) < 0 := by
  rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_neg_iff, LinearEquiv.coe_det]

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