Ordered instances on submodules

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

• S.toOrderedAddCommMonoid = Function.Injective.orderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

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

• S.toLinearOrderedAddCommMonoid = Function.Injective.linearOrderedAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

• S.toOrderedCancelAddCommMonoid = Function.Injective.orderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

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

• S.toLinearOrderedCancelAddCommMonoid = Function.Injective.linearOrderedCancelAddCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

• S.toOrderedAddCommGroup = Function.Injective.orderedAddCommGroup Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

• S.toLinearOrderedAddCommGroup = Function.Injective.linearOrderedAddCommGroup Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯