English
When the index has cardinality equal to the finite dimension, Orientation.map acts by multiplying by the inverse determinant on the base orientation.
Русский
При совпадении кардинальности индексов и конечной размерности ориентация отображается через обратную детерминанту.
LaTeX
$$$$ Orientation.map ι f x = (\\det f)^{-1} \\cdot x $$$$
Lean4
/-- The value of `Orientation.map` when the index type has cardinality equal to the finite
dimension, in terms of `f.det`. -/
theorem map_eq_det_inv_smul [FiniteDimensional R M] (x : Orientation R M ι) (f : M ≃ₗ[R] M)
(h : Fintype.card ι = finrank R M) : Orientation.map ι f x = (LinearEquiv.det f)⁻¹ • x :=
haveI e := (finBasis R M).reindex (Fintype.equivFinOfCardEq h).symm
e.map_orientation_eq_det_inv_smul x f
