Theorems · Theorem · linear algebra

Orientation.ne_iff_eq_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 ι] [FiniteDimensional R M]
  (x₁ x₂ : Orientation R M ι), Fintype.card ι = Module.finrank R M → (x₁ ≠ x₂ ↔ x₁ = -x₂)

If the index type has cardinality equal to the finite dimension, an orientation equals the negation of another orientation if and only if they are not equal.

Defined in

Mathlib.LinearAlgebra.Orientation

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingAddCommGroupModuleFintypeFiniteDimensional