Mathlib.Algebra.Order.Positive.Ring

Positive.instAddSubtypeLtOfNat_mathlib instance

: Add { x : M // 0 < x }

Full source

instance : Add { x : M // 0 < x } :=
  ⟨fun x y => ⟨x + y, add_pos x.2 y.2⟩⟩

Addition Structure on Positive Elements

Informal description

For any type $M$ with a zero element and a positive cone, the set $\{x : M \mid 0 < x\}$ has a canonical addition structure inherited from $M$.

Positive.coe_add theorem

(x y : { x : M // 0 < x }) : ↑(x + y) = (x + y : M)

Full source

@[simp, norm_cast]
theorem coe_add (x y : { x : M // 0 < x }) : ↑(x + y) = (x + y : M) :=
  rfl

Canonical inclusion preserves addition for positive elements

Informal description

For any elements $x$ and $y$ in the set $\{x : M \mid 0 < x\}$ of positive elements of $M$, the canonical inclusion map $\uparrow$ satisfies $\uparrow(x + y) = \uparrow x + \uparrow y$ in $M$.

Positive.addSemigroup instance

: AddSemigroup { x : M // 0 < x }

Full source

instance addSemigroup : AddSemigroup { x : M // 0 < x } := fast_instance%
  Subtype.coe_injective.addSemigroup _ coe_add

Additive Semigroup Structure on Positive Elements

Informal description

For any type $M$ with a zero element and a positive cone, the set $\{x : M \mid 0 < x\}$ forms an additive semigroup under the addition inherited from $M$.

Positive.addCommSemigroup instance

{M : Type*} [AddCommMonoid M] [Preorder M] [AddLeftStrictMono M] : AddCommSemigroup { x : M // 0 < x }

Full source

instance addCommSemigroup {M : Type*} [AddCommMonoid M] [Preorder M]
    [AddLeftStrictMono M] : AddCommSemigroup { x : M // 0 < x } := fast_instance%
  Subtype.coe_injective.addCommSemigroup _ coe_add

Commutative Additive Semigroup Structure on Positive Elements

Informal description

For any additively commutative monoid $M$ with a preorder and strictly increasing left addition, the set $\{x : M \mid 0 < x\}$ of positive elements forms an additively commutative semigroup under the inherited addition.

Positive.addLeftCancelSemigroup instance

{M : Type*} [AddLeftCancelMonoid M] [Preorder M] [AddLeftStrictMono M] : AddLeftCancelSemigroup { x : M // 0 < x }

Full source

instance addLeftCancelSemigroup {M : Type*} [AddLeftCancelMonoid M] [Preorder M]
    [AddLeftStrictMono M] : AddLeftCancelSemigroup { x : M // 0 < x } := fast_instance%
  Subtype.coe_injective.addLeftCancelSemigroup _ coe_add

Left-Cancellative Additive Semigroup Structure on Positive Elements

Informal description

For any type $M$ with a left-cancellative additive monoid structure, a preorder, and strictly increasing left addition, the set $\{x : M \mid 0 < x\}$ forms a left-cancellative additive semigroup under the inherited addition.

Positive.addRightCancelSemigroup instance

{M : Type*} [AddRightCancelMonoid M] [Preorder M] [AddLeftStrictMono M] : AddRightCancelSemigroup { x : M // 0 < x }

Full source

instance addRightCancelSemigroup {M : Type*} [AddRightCancelMonoid M] [Preorder M]
    [AddLeftStrictMono M] : AddRightCancelSemigroup { x : M // 0 < x } := fast_instance%
  Subtype.coe_injective.addRightCancelSemigroup _ coe_add

Right-Cancellative Additive Semigroup Structure on Positive Elements

Informal description

For any type $M$ with a right-cancellative additive monoid structure, a preorder, and strictly increasing left addition, the set $\{x : M \mid 0 < x\}$ of positive elements forms a right-cancellative additive semigroup under the inherited addition.

Positive.addLeftStrictMono instance

: AddLeftStrictMono { x : M // 0 < x }

Full source

instance addLeftStrictMono : AddLeftStrictMono { x : M // 0 < x } :=
  ⟨fun _ y z hyz => Subtype.coe_lt_coe.1 <| add_lt_add_left (show (y : M) < z from hyz) _⟩

Left Strict Monotonicity of Addition on Positive Elements

Informal description

For any type $M$ with a strict order and an addition operation that is strictly monotone on the left (i.e., $a < b$ implies $c + a < c + b$ for all $a, b, c \in M$), the set $\{x \in M \mid 0 < x\}$ of positive elements in $M$ inherits this property.

Positive.addRightStrictMono instance

[AddRightStrictMono M] : AddRightStrictMono { x : M // 0 < x }

Full source

instance addRightStrictMono [AddRightStrictMono M] : AddRightStrictMono { x : M // 0 < x } :=
  ⟨fun _ y z hyz => Subtype.coe_lt_coe.1 <| add_lt_add_right (show (y : M) < z from hyz) _⟩

Right Strict Monotonicity of Addition on Positive Elements

Informal description

For any type $M$ with a strict order and an addition operation that is strictly monotone on the right (i.e., $a < b$ implies $a + c < b + c$ for all $a, b, c \in M$), the set $\{x \in M \mid 0 < x\}$ of positive elements in $M$ inherits this property.

Positive.addLeftReflectLT instance

[AddLeftReflectLT M] : AddLeftReflectLT { x : M // 0 < x }

Full source

instance addLeftReflectLT [AddLeftReflectLT M] : AddLeftReflectLT { x : M // 0 < x } :=
  ⟨fun _ _ _ h => Subtype.coe_lt_coe.1 <| lt_of_add_lt_add_left h⟩

Left Order Reflection for Addition on Positive Elements

Informal description

For any type $M$ with a strict order and an addition operation that reflects the order from the left (i.e., $a + b < a + c$ implies $b < c$ for all $a, b, c \in M$), the set $\{x \in M \mid 0 < x\}$ of positive elements in $M$ inherits this property.

Positive.addRightReflectLT instance

[AddRightReflectLT M] : AddRightReflectLT { x : M // 0 < x }

Full source

instance addRightReflectLT [AddRightReflectLT M] : AddRightReflectLT { x : M // 0 < x } :=
  ⟨fun _ _ _ h => Subtype.coe_lt_coe.1 <| lt_of_add_lt_add_right h⟩

Right Order Reflection for Addition on Positive Elements

Informal description

For any type $M$ with a strict order and an addition operation that reflects the order from the right (i.e., $a + c < b + c$ implies $a < b$ for all $a, b, c \in M$), the set $\{x : M \mid 0 < x\}$ of positive elements in $M$ inherits this property.

Positive.addLeftReflectLE instance

[AddLeftReflectLE M] : AddLeftReflectLE { x : M // 0 < x }

Full source

instance addLeftReflectLE [AddLeftReflectLE M] : AddLeftReflectLE { x : M // 0 < x } :=
  ⟨fun _ _ _ h => Subtype.coe_le_coe.1 <| le_of_add_le_add_left h⟩

Left Order Reflection for Addition on Positive Elements

Informal description

For any type $M$ with a preorder and an addition operation that reflects the order from the left (i.e., $a + b \leq a + c$ implies $b \leq c$ for all $a, b, c \in M$), the set $\{x : M \mid 0 < x\}$ of positive elements in $M$ inherits this property.

Positive.addRightReflectLE instance

[AddRightReflectLE M] : AddRightReflectLE { x : M // 0 < x }

Full source

instance addRightReflectLE [AddRightReflectLE M] : AddRightReflectLE { x : M // 0 < x } :=
  ⟨fun _ _ _ h => Subtype.coe_le_coe.1 <| le_of_add_le_add_right h⟩

Right Order Reflection for Addition on Positive Elements

Informal description

For any type $M$ with a preorder and an addition operation that reflects the order from the right (i.e., $a + c \leq b + c$ implies $a \leq b$ for all $a, b, c \in M$), the set $\{x \in M \mid 0 < x\}$ of positive elements in $M$ inherits this property.

Positive.addLeftMono instance

[AddMonoid M] [PartialOrder M] [AddLeftStrictMono M] : AddLeftMono { x : M // 0 < x }

Full source

instance addLeftMono [AddMonoid M] [PartialOrder M] [AddLeftStrictMono M] :
    AddLeftMono { x : M // 0 < x } :=
  ⟨@fun _ _ _ h₁ => StrictMono.monotone (fun _ _ h => add_lt_add_left h _) h₁⟩

Left Monotonicity of Addition on Positive Elements

Informal description

For any additively left-strictly monotone add monoid $M$ with a partial order, the set of positive elements $\{x \in M \mid 0 < x\}$ inherits the property of being additively left-monotone. That is, for any positive elements $a, b, c \in M$, if $a \leq b$ then $c + a \leq c + b$.

Positive.instMulSubtypeLtOfNat_mathlib instance

: Mul { x : R // 0 < x }

Full source

instance : Mul { x : R // 0 < x } :=
  ⟨fun x y => ⟨x * y, mul_pos x.2 y.2⟩⟩

Multiplication on Positive Elements

Informal description

For any type $R$ with a partial order and a multiplication operation, the set of positive elements $\{x : R \mid 0 < x\}$ is equipped with a multiplication operation inherited from $R$.

Positive.val_mul theorem

(x y : { x : R // 0 < x }) : ↑(x * y) = (x * y : R)

Full source

@[simp]
theorem val_mul (x y : { x : R // 0 < x }) : ↑(x * y) = (x * y : R) :=
  rfl

Multiplication Commutes with Embedding of Positive Elements

Informal description

For any two positive elements $x, y$ in a partially ordered ring $R$ (i.e., $x, y \in R$ with $0 < x$ and $0 < y$), the canonical embedding of their product in $R$ equals the product of their embeddings. In other words, $(x \cdot y : R) = (x : R) \cdot (y : R)$.

Positive.instPowSubtypeLtOfNatNat_mathlib instance

: Pow { x : R // 0 < x } ℕ

Full source

instance : Pow { x : R // 0 < x } ℕ :=
  ⟨fun x n => ⟨(x : R) ^ n , pow_pos x.2 n⟩⟩

Power Operation on Positive Elements

Informal description

For any type $R$ with a partial order and a zero element, the set of positive elements $\{x : R \mid 0 < x\}$ is equipped with a natural power operation $x^n$ for natural numbers $n$, where the operation is inherited from the power operation on $R$.

Positive.val_pow theorem

(x : { x : R // 0 < x }) (n : ℕ) : ↑(x ^ n) = (x : R) ^ n

Full source

@[simp]
theorem val_pow (x : { x : R // 0 < x }) (n : ℕ) :
    ↑(x ^ n) = (x : R) ^ n :=
  rfl

Power operation commutes with embedding of positive elements

Informal description

For any positive element $x$ in a partially ordered ring $R$ (i.e., $x \in R$ with $0 < x$) and any natural number $n$, the canonical embedding of $x^n$ in $R$ equals the $n$-th power of $x$ in $R$. In other words, $(x^n : R) = (x : R)^n$.

Positive.instSemigroupSubtypeLtOfNat instance

: Semigroup { x : R // 0 < x }

Full source

instance : Semigroup { x : R // 0 < x } := fast_instance%
  Subtype.coe_injective.semigroup Subtype.val val_mul

Semigroup Structure on Positive Elements

Informal description

For any type $R$ with a partial order and a multiplication operation, the set of positive elements $\{x : R \mid 0 < x\}$ forms a semigroup under the multiplication inherited from $R$.

Positive.instDistribSubtypeLtOfNat instance

: Distrib { x : R // 0 < x }

Full source

instance : Distrib { x : R // 0 < x } := fast_instance%
  Subtype.coe_injective.distrib _ coe_add val_mul

Distributive Multiplication on Positive Elements

Informal description

For any type $R$ with a partial order and a multiplication operation, the set of positive elements $\{x : R \mid 0 < x\}$ is equipped with a distributive multiplication operation inherited from $R$.

Positive.instOneSubtypeLtOfNat instance

: One { x : R // 0 < x }

Full source

instance : One { x : R // 0 < x } :=
  ⟨⟨1, one_pos⟩⟩

The One Element of Positive Elements in an Ordered Type

Informal description

For any type $R$ with a zero element and a strict order, the set $\{x : R \mid 0 < x\}$ has a canonical one element.

Positive.val_one theorem

: ((1 : { x : R // 0 < x }) : R) = 1

Full source

@[simp]
theorem val_one : ((1 : { x : R // 0 < x }) : R) = 1 :=
  rfl

Inclusion of Positive One Equals One

Informal description

For any ordered type $R$ with a zero element and a strict order, the canonical inclusion map from the set of positive elements $\{x : R \mid 0 < x\}$ to $R$ maps the multiplicative identity element $1$ to the multiplicative identity element $1$ in $R$.

Positive.instMonoidSubtypeLtOfNat instance

: Monoid { x : R // 0 < x }

Full source

instance : Monoid { x : R // 0 < x } := fast_instance%
  Subtype.coe_injective.monoid _ val_one val_mul val_pow

Monoid Structure on Positive Elements

Informal description

For any type $R$ with a partial order and a multiplication operation, the set of positive elements $\{x : R \mid 0 < x\}$ forms a monoid under the multiplication inherited from $R$.

Positive.commMonoid instance

[CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] : CommMonoid { x : R // 0 < x }

Full source

instance commMonoid [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
    CommMonoid { x : R // 0 < x } := fast_instance%
  Subtype.coe_injective.commMonoid (M₂ := R) (Subtype.val) val_one val_mul val_pow

Commutative Monoid Structure on Positive Elements of a Strict Ordered Ring

Informal description

For any commutative semiring $R$ with a partial order that forms a strict ordered ring, the set of positive elements $\{x : R \mid 0 < x\}$ forms a commutative monoid under the multiplication inherited from $R$.

Positive.isOrderedMonoid instance

[CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] : IsOrderedMonoid { x : R // 0 < x }

Full source

instance isOrderedMonoid [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
    IsOrderedMonoid { x : R // 0 < x } :=
  { mul_le_mul_left := fun _ _ hxy c =>
      Subtype.coe_le_coe.1 <| mul_le_mul_of_nonneg_left hxy c.2.le }

Ordered Monoid Structure on Positive Elements of a Strict Ordered Ring

Informal description

For any commutative semiring $R$ with a partial order that forms a strict ordered ring, the set of positive elements $\{x \in R \mid 0 < x\}$ forms an ordered monoid under the multiplication inherited from $R$. This means that the multiplication operation is monotone in both arguments with respect to the inherited partial order.

Positive.isOrderedCancelMonoid instance

[CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R] : IsOrderedCancelMonoid { x : R // 0 < x }

Full source

/-- If `R` is a nontrivial linear ordered commutative semiring, then `{x : R // 0 < x}` is a linear
ordered cancellative commutative monoid. -/
instance isOrderedCancelMonoid [CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R] :
    IsOrderedCancelMonoid { x : R // 0 < x } :=
  { le_of_mul_le_mul_left := fun a _ _ h => Subtype.coe_le_coe.1 <| (mul_le_mul_left a.2).1 h }

Positive Elements of a Strict Ordered Ring Form a Linearly Ordered Cancellative Commutative Monoid

Informal description

For any commutative semiring $R$ with a linear order that forms a strict ordered ring, the set of positive elements $\{x \in R \mid 0 < x\}$ forms a linearly ordered cancellative commutative monoid under the multiplication inherited from $R$.