Documentation

Mathlib.Algebra.Module.Submodule.Order

Ordered instances on submodules #

source
instance Submodule.toOrderedAddCommMonoid {R : Type u_1} {M : Type u_2} [Semiring R] [OrderedAddCommMonoid M] [Module R M] (S : Submodule R M) :
OrderedAddCommMonoid ↥S

A submodule of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

Equations
source
instance Submodule.toLinearOrderedAddCommMonoid {R : Type u_1} {M : Type u_2} [Semiring R] [LinearOrderedAddCommMonoid M] [Module R M] (S : Submodule R M) :
LinearOrderedAddCommMonoid ↥S

A submodule of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

Equations
source
instance Submodule.toOrderedCancelAddCommMonoid {R : Type u_1} {M : Type u_2} [Semiring R] [OrderedCancelAddCommMonoid M] [Module R M] (S : Submodule R M) :
OrderedCancelAddCommMonoid ↥S

A submodule of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations
source
instance Submodule.toLinearOrderedCancelAddCommMonoid {R : Type u_1} {M : Type u_2} [Semiring R] [LinearOrderedCancelAddCommMonoid M] [Module R M] (S : Submodule R M) :
LinearOrderedCancelAddCommMonoid ↥S

A submodule of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

Equations
  • One or more equations did not get rendered due to their size.
source
instance Submodule.toOrderedAddCommGroup {R : Type u_1} {M : Type u_2} [Ring R] [OrderedAddCommGroup M] [Module R M] (S : Submodule R M) :
OrderedAddCommGroup ↥S

A submodule of an OrderedAddCommGroup is an OrderedAddCommGroup.

Equations
source
instance Submodule.toLinearOrderedAddCommGroup {R : Type u_1} {M : Type u_2} [Ring R] [LinearOrderedAddCommGroup M] [Module R M] (S : Submodule R M) :
LinearOrderedAddCommGroup ↥S

A submodule of a LinearOrderedAddCommGroup is a LinearOrderedAddCommGroup.

Equations