Documentation

Mathlib.Algebra.Order.Ring.Canonical

Canonically ordered rings and semirings. #

@[deprecated "Use `[OrderedCommSemiring R] [CanonicallyOrderedAdd R] [NoZeroDivisors R]` instead." (since := "2025-01-13")]

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.

Instances For
    theorem Odd.pos {R : Type u} [Semiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Nontrivial R] {a : R} :
    Odd a0 < a
    @[simp]
    theorem CanonicallyOrderedAdd.mul_pos {R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] {a b : R} :
    0 < a * b 0 < a 0 < b
    theorem CanonicallyOrderedAdd.pow_pos {R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] {a : R} (ha : 0 < a) (n : ) :
    0 < a ^ n
    theorem CanonicallyOrderedAdd.mul_lt_mul_of_lt_of_lt {R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [PosMulStrictMono R] {a b c d : R} (hab : a < b) (hcd : c < d) :
    a * c < b * d
    theorem AddLECancellable.mul_tsub {R : Type u} [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [IsTotal R fun (x1 x2 : R) => x1 x2] {a b c : R} (h : AddLECancellable (a * c)) :
    a * (b - c) = a * b - a * c
    theorem AddLECancellable.tsub_mul {R : Type u} [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [IsTotal R fun (x1 x2 : R) => x1 x2] [MulRightMono R] {a b c : R} (h : AddLECancellable (b * c)) :
    (a - b) * c = a * c - b * c
    theorem mul_tsub {R : Type u} [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [IsTotal R fun (x1 x2 : R) => x1 x2] [AddLeftReflectLE R] (a b c : R) :
    a * (b - c) = a * b - a * c
    theorem tsub_mul {R : Type u} [NonUnitalNonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [IsTotal R fun (x1 x2 : R) => x1 x2] [AddLeftReflectLE R] [MulRightMono R] (a b c : R) :
    (a - b) * c = a * c - b * c
    theorem mul_tsub_one {R : Type u} [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [IsTotal R fun (x1 x2 : R) => x1 x2] [AddLeftReflectLE R] (a b : R) :
    a * (b - 1) = a * b - a
    theorem tsub_one_mul {R : Type u} [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [IsTotal R fun (x1 x2 : R) => x1 x2] [MulRightMono R] [AddLeftReflectLE R] (a b : R) :
    (a - 1) * b = a * b - b
    theorem mul_self_tsub_mul_self {R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [IsTotal R fun (x1 x2 : R) => x1 x2] [AddLeftReflectLE R] (a b : R) :
    a * a - b * b = (a + b) * (a - b)

    The tsub version of mul_self_sub_mul_self. Notably, this holds for Nat and NNReal.

    theorem sq_tsub_sq {R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [IsTotal R fun (x1 x2 : R) => x1 x2] [AddLeftReflectLE R] (a b : R) :
    a ^ 2 - b ^ 2 = (a + b) * (a - b)

    The tsub version of sq_sub_sq. Notably, this holds for Nat and NNReal.

    theorem mul_self_tsub_one {R : Type u} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Sub R] [OrderedSub R] [IsTotal R fun (x1 x2 : R) => x1 x2] [AddLeftReflectLE R] (a : R) :
    a * a - 1 = (a + 1) * (a - 1)