Documentation

Mathlib.Algebra.Order.Ring.Canonical

Canonically ordered rings and semirings. #

TODO #

We're still missing some typeclasses, like

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 : ααα
  • add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • nsmul : αα
  • nsmul_zero : ∀ (x : α), AddMonoid.nsmul 0 x = 0
  • nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
  • add_comm : ∀ (a b : α), a + b = b + a
  • le : ααProp
  • lt : ααProp
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
  • bot : α
  • bot_le : ∀ (a : α), a
  • exists_add_of_le : ∀ {a b : α}, a b∃ (c : α), b = a + c
  • le_self_add : ∀ (a b : α), a a + b
  • mul : ααα
  • left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c

    Multiplication is left distributive over addition

  • right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c

    Multiplication is right distributive over addition

  • zero_mul : ∀ (a : α), 0 * a = 0

    Zero is a left absorbing element for multiplication

  • mul_zero : ∀ (a : α), a * 0 = 0

    Zero is a right absorbing element for multiplication

  • mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

    Multiplication is associative

  • one : α
  • one_mul : ∀ (a : α), 1 * a = a

    One is a left neutral element for multiplication

  • mul_one : ∀ (a : α), a * 1 = a

    One is a right neutral element for multiplication

  • natCast : α
  • natCast_zero : NatCast.natCast 0 = 0

    The canonical map ℕ → R sends 0 : ℕ to 0 : R.

  • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1

    The canonical map ℕ → R is a homomorphism.

  • npow : αα

    Raising to the power of a natural number.

  • npow_zero : ∀ (x : α), CanonicallyOrderedCommSemiring.npow 0 x = 1

    Raising to the power (0 : ℕ) gives 1.

  • npow_succ : ∀ (n : ) (x : α), CanonicallyOrderedCommSemiring.npow (n + 1) x = CanonicallyOrderedCommSemiring.npow n x * x

    Raising to the power (n + 1 : ℕ) behaves as expected.

  • mul_comm : ∀ (a b : α), a * b = b * a

    Multiplication is commutative in a commutative multiplicative magma.

  • eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : α}, a * b = 0a = 0 b = 0

    No zero divisors.

Instances
    theorem CanonicallyOrderedCommSemiring.eq_zero_or_eq_zero_of_mul_eq_zero {α : Type u_1} [self : CanonicallyOrderedCommSemiring α] {a : α} {b : α} :
    a * b = 0a = 0 b = 0

    No zero divisors.

    theorem Odd.pos {α : Type u} [CanonicallyOrderedCommSemiring α] {a : α} [Nontrivial α] :
    Odd a0 < a
    @[instance 100]
    instance CanonicallyOrderedCommSemiring.toCovariantClassMulLE {α : Type u} [CanonicallyOrderedCommSemiring α] :
    CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2
    Equations
    • =
    @[instance 100]
    Equations
    @[instance 100]
    Equations
    @[simp]
    theorem CanonicallyOrderedCommSemiring.mul_pos {α : Type u} [CanonicallyOrderedCommSemiring α] {a : α} {b : α} :
    0 < a * b 0 < a 0 < b
    theorem CanonicallyOrderedCommSemiring.pow_pos {α : Type u} [CanonicallyOrderedCommSemiring α] {a : α} (ha : 0 < a) (n : ) :
    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) :
    a * c < b * d
    theorem AddLECancellable.mul_tsub {α : Type u} [CanonicallyOrderedCommSemiring α] {a : α} {b : α} {c : α} [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 x2] (h : AddLECancellable (a * c)) :
    a * (b - c) = a * b - a * c
    theorem AddLECancellable.tsub_mul {α : Type u} [CanonicallyOrderedCommSemiring α] {a : α} {b : α} {c : α} [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 x2] (h : AddLECancellable (b * c)) :
    (a - b) * c = a * c - b * c
    theorem mul_tsub {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) (c : α) :
    a * (b - c) = a * b - a * c
    theorem tsub_mul {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) (c : α) :
    (a - b) * c = a * c - b * c
    theorem mul_tsub_one {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
    a * (b - 1) = a * b - a
    theorem tsub_one_mul {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
    (a - 1) * b = a * b - b
    theorem mul_self_tsub_mul_self {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
    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 {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
    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 {α : Type u} [CanonicallyOrderedCommSemiring α] [Sub α] [OrderedSub α] [IsTotal α fun (x1 x2 : α) => x1 x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
    a * a - 1 = (a + 1) * (a - 1)