Theorems · Theorem · linear algebra

Orientation.map_eq_neg_iff_det_neg

∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] (x : Orientation R M ι)
  (f : M ≃ₗ[R] M), Fintype.card ι = Module.finrank R M → ((Orientation.map ι f) x = -x ↔ LinearMap.det ↑f < 0)

If the index type has cardinality equal to the finite dimension, composing an alternating map with the same linear equiv on each argument gives the negation of that orientation if and only if the determinant is negative.

Defined in

Mathlib.LinearAlgebra.Orientation

Cited by

0 results in Mathlib

Foundations

Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsStrictOrderedRingAddCommGroupModuleFintype