Theorems · Theorem · linear algebra

Orientation.reindex_neg

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι') (x : Orientation R M ι),
  (Orientation.reindex R M e) (-x) = -(Orientation.reindex R M e) x

Defined in

Mathlib.LinearAlgebra.Orientation

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingPartialOrderIsStrictOrderedRingAddCommGroupModule