Theorems · Definition · linear algebra

Module.Oriented.positiveOrientation

{R : Type u_1} →
  {inst : CommSemiring R} →
    {inst_1 : PartialOrder R} →
      {inst_2 : IsStrictOrderedRing R} →
        {M : Type u_2} →
          {inst_3 : AddCommMonoid M} →
            {inst_4 : Module R M} → {ι : Type u_4} → [self : Module.Oriented R M ι] → Orientation R M ι

Fix a positive orientation.

Defined in

Mathlib.LinearAlgebra.Orientation

Cited by

15 results in Mathlib

Foundations

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

Assumes

Module.Oriented