Theorems · Inductive type · order theory

PositiveLinearMap

(R : Type u_1) →
  (E₁ : Type u_2) →
    (E₂ : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E₁] →
          [PartialOrder E₁] →
            [inst_3 : AddCommMonoid E₂] → [PartialOrder E₂] → [Module R E₁] → [Module R E₂] → Type (max u_2 u_3)

A positive linear map is a linear map that is also an order homomorphism.

Defined in

Mathlib.Algebra.Order.Module.PositiveLinearMap

Cited by

52 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

SemiringAddCommMonoidPartialOrderAddCommMonoidPartialOrderModuleModule