Theorems · Inductive type · linear algebra

Module.Oriented

(R : Type u_1) →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [IsStrictOrderedRing R] →
        (M : Type u_2) → [inst_3 : AddCommMonoid M] → [Module R M] → Type u_4 → Type (max (max u_1 u_2) u_4)

A type class fixing an orientation of a module.

Defined in

Mathlib.LinearAlgebra.Orientation

Cited by

190 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 8 definitions · uses no axioms

Assumes

CommSemiringPartialOrderIsStrictOrderedRingAddCommMonoidModule