orientation_comp_linearEquiv_eq_iff_det_pos

English

Composing a basis with a linear equivalence preserves orientation if and only if the determinant of the equivalence is positive.

Русский

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

LaTeX

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

Lean4

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

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