Canonically ordered rings and semirings. #
CanonicallyOrderedCommSemiring
CanonicallyOrderedAddCommMonoid
& multiplication &*
respects≤
& no zero divisorsCommSemiring
&a ≤ b ↔ ∃ c, b = a + c
& no zero divisors
TODO #
We're still missing some typeclasses, like
CanonicallyOrderedSemiring
They have yet to come up in practice.
class
CanonicallyOrderedCommSemiring
(α : Type u_1)
extends CanonicallyOrderedAddCommMonoid α, CommSemiring α :
Type u_1
A canonically ordered commutative semiring is an ordered, commutative semiring in which a ≤ b
iff there exists c
with b = a + c
. This is satisfied by the natural numbers, for example, but
not the integers or other ordered groups.
- add : α → α → α
- zero : α
- nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
- bot : α
- exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ (c : α), b = a + c
- le_self_add : ∀ (a b : α), a ≤ a + b
- mul : α → α → α
- one : α
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow_zero : ∀ (x : α), CanonicallyOrderedCommSemiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : α), CanonicallyOrderedCommSemiring.npow (n + 1) x = CanonicallyOrderedCommSemiring.npow n x * x
No zero divisors.
Instances
theorem
CanonicallyOrderedCommSemiring.toNoZeroDivisors
{α : Type u}
[CanonicallyOrderedCommSemiring α]
:
theorem
CanonicallyOrderedCommSemiring.toMulLeftMono
{α : Type u}
[CanonicallyOrderedCommSemiring α]
:
@[instance 100]
instance
CanonicallyOrderedCommSemiring.toOrderedCommMonoid
{α : Type u}
[CanonicallyOrderedCommSemiring α]
:
Equations
- CanonicallyOrderedCommSemiring.toOrderedCommMonoid = OrderedCommMonoid.mk ⋯
@[instance 100]
instance
CanonicallyOrderedCommSemiring.toOrderedCommSemiring
{α : Type u}
[CanonicallyOrderedCommSemiring α]
:
Equations
- CanonicallyOrderedCommSemiring.toOrderedCommSemiring = OrderedCommSemiring.mk ⋯
@[simp]
theorem
CanonicallyOrderedCommSemiring.mul_pos
{α : Type u}
[CanonicallyOrderedCommSemiring α]
{a b : α}
:
theorem
CanonicallyOrderedCommSemiring.pow_pos
{α : Type u}
[CanonicallyOrderedCommSemiring α]
{a : α}
(ha : 0 < a)
(n : ℕ)
:
theorem
CanonicallyOrderedCommSemiring.mul_lt_mul_of_lt_of_lt
{α : Type u}
[CanonicallyOrderedCommSemiring α]
{a b c d : α}
[PosMulStrictMono α]
(hab : a < b)
(hcd : c < d)
:
theorem
AddLECancellable.mul_tsub
{α : Type u}
[CanonicallyOrderedCommSemiring α]
{a b c : α}
[Sub α]
[OrderedSub α]
[IsTotal α fun (x1 x2 : α) => x1 ≤ x2]
(h : AddLECancellable (a * c))
:
theorem
AddLECancellable.tsub_mul
{α : Type u}
[CanonicallyOrderedCommSemiring α]
{a b c : α}
[Sub α]
[OrderedSub α]
[IsTotal α fun (x1 x2 : α) => x1 ≤ x2]
(h : AddLECancellable (b * c))
:
theorem
mul_tsub
{α : Type u}
[CanonicallyOrderedCommSemiring α]
[Sub α]
[OrderedSub α]
[IsTotal α fun (x1 x2 : α) => x1 ≤ x2]
[AddLeftReflectLE α]
(a b c : α)
:
theorem
tsub_mul
{α : Type u}
[CanonicallyOrderedCommSemiring α]
[Sub α]
[OrderedSub α]
[IsTotal α fun (x1 x2 : α) => x1 ≤ x2]
[AddLeftReflectLE α]
(a b c : α)
:
theorem
mul_tsub_one
{α : Type u}
[CanonicallyOrderedCommSemiring α]
[Sub α]
[OrderedSub α]
[IsTotal α fun (x1 x2 : α) => x1 ≤ x2]
[AddLeftReflectLE α]
(a b : α)
:
theorem
tsub_one_mul
{α : Type u}
[CanonicallyOrderedCommSemiring α]
[Sub α]
[OrderedSub α]
[IsTotal α fun (x1 x2 : α) => x1 ≤ x2]
[AddLeftReflectLE α]
(a b : α)
:
theorem
mul_self_tsub_mul_self
{α : Type u}
[CanonicallyOrderedCommSemiring α]
[Sub α]
[OrderedSub α]
[IsTotal α fun (x1 x2 : α) => x1 ≤ x2]
[AddLeftReflectLE α]
(a b : α)
:
The tsub
version of mul_self_sub_mul_self
. Notably, this holds for Nat
and NNReal
.
theorem
sq_tsub_sq
{α : Type u}
[CanonicallyOrderedCommSemiring α]
[Sub α]
[OrderedSub α]
[IsTotal α fun (x1 x2 : α) => x1 ≤ x2]
[AddLeftReflectLE α]
(a b : α)
:
The tsub
version of sq_sub_sq
. Notably, this holds for Nat
and NNReal
.
theorem
mul_self_tsub_one
{α : Type u}
[CanonicallyOrderedCommSemiring α]
[Sub α]
[OrderedSub α]
[IsTotal α fun (x1 x2 : α) => x1 ≤ x2]
[AddLeftReflectLE α]
(a : α)
: