Algebraic structures on the set of positive numbers #
In this file we define various instances (AddSemigroup
, OrderedCommMonoid
etc) on the
type {x : R // 0 < x}
. In each case we try to require the weakest possible typeclass
assumptions on R
but possibly, there is a room for improvements.
instance
Positive.instAddSubtypeLtToLTOfNatToOfNat0ToZero
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
:
instance
Positive.addSemigroup
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
:
AddSemigroup { x // 0 < x }
Equations
- Positive.addSemigroup = Function.Injective.addSemigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : { x // 0 < x }), ↑(x + y) = ↑x + ↑y)
instance
Positive.addCommSemigroup
{M : Type u_1}
[inst : AddCommMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
:
AddCommSemigroup { x // 0 < x }
Equations
- Positive.addCommSemigroup = Function.Injective.addCommSemigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : { x // 0 < x }), ↑(x + y) = ↑x + ↑y)
instance
Positive.addLeftCancelSemigroup
{M : Type u_1}
[inst : AddLeftCancelMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
:
AddLeftCancelSemigroup { x // 0 < x }
Equations
- Positive.addLeftCancelSemigroup = Function.Injective.addLeftCancelSemigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : { x // 0 < x }), ↑(x + y) = ↑x + ↑y)
instance
Positive.addRightCancelSemigroup
{M : Type u_1}
[inst : AddRightCancelMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
:
AddRightCancelSemigroup { x // 0 < x }
Equations
- Positive.addRightCancelSemigroup = Function.Injective.addRightCancelSemigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : { x // 0 < x }), ↑(x + y) = ↑x + ↑y)
instance
Positive.covariantClass_add_lt
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
:
CovariantClass { x // 0 < x } { x // 0 < x } (fun x x_1 => x + x_1) fun x x_1 => x < x_1
instance
Positive.covariantClass_swap_add_lt
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1]
:
CovariantClass { x // 0 < x } { x // 0 < x } (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
instance
Positive.contravariantClass_add_lt
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
:
ContravariantClass { x // 0 < x } { x // 0 < x } (fun x x_1 => x + x_1) fun x x_1 => x < x_1
instance
Positive.contravariantClass_swap_add_lt
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst : ContravariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1]
:
ContravariantClass { x // 0 < x } { x // 0 < x } (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
instance
Positive.contravariantClass_add_le
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
:
ContravariantClass { x // 0 < x } { x // 0 < x } (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
instance
Positive.contravariantClass_swap_add_le
{M : Type u_1}
[inst : AddMonoid M]
[inst : Preorder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
[inst : ContravariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
:
ContravariantClass { x // 0 < x } { x // 0 < x } (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
instance
Positive.covariantClass_add_le
{M : Type u_1}
[inst : AddMonoid M]
[inst : PartialOrder M]
[inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
:
CovariantClass { x // 0 < x } { x // 0 < x } (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
instance
Positive.instMulSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring
{R : Type u_1}
[inst : StrictOrderedSemiring R]
:
@[simp]
theorem
Positive.val_mul
{R : Type u_1}
[inst : StrictOrderedSemiring R]
(x : { x // 0 < x })
(y : { x // 0 < x })
:
instance
Positive.instPowSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiringNat
{R : Type u_1}
[inst : StrictOrderedSemiring R]
:
@[simp]
theorem
Positive.val_pow
{R : Type u_1}
[inst : StrictOrderedSemiring R]
(x : { x // 0 < x })
(n : ℕ)
:
instance
Positive.instSemigroupSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring
{R : Type u_1}
[inst : StrictOrderedSemiring R]
:
Equations
- One or more equations did not get rendered due to their size.
instance
Positive.instDistribSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring
{R : Type u_1}
[inst : StrictOrderedSemiring R]
:
Equations
- One or more equations did not get rendered due to their size.
instance
Positive.instOneSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring
{R : Type u_1}
[inst : StrictOrderedSemiring R]
[inst : Nontrivial R]
:
@[simp]
theorem
Positive.val_one
{R : Type u_1}
[inst : StrictOrderedSemiring R]
[inst : Nontrivial R]
:
↑1 = 1
instance
Positive.instMonoidSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring
{R : Type u_1}
[inst : StrictOrderedSemiring R]
[inst : Nontrivial R]
:
Equations
- One or more equations did not get rendered due to their size.
instance
Positive.orderedCommMonoid
{R : Type u_1}
[inst : StrictOrderedCommSemiring R]
[inst : Nontrivial R]
:
OrderedCommMonoid { x // 0 < x }
Equations
- One or more equations did not get rendered due to their size.
instance
Positive.linearOrderedCancelCommMonoid
{R : Type u_1}
[inst : LinearOrderedCommSemiring R]
:
LinearOrderedCancelCommMonoid { x // 0 < x }
If R
is a nontrivial linear ordered commutative semiring, then {x : R // 0 < x}
is a linear
ordered cancellative commutative monoid.
Equations
- One or more equations did not get rendered due to their size.