mathlib3 documentation

algebra.order.ring.canonical

Canoncially ordered rings and semirings. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

TODO #

We're still missing some typeclasses, like

@[class]
structure canonically_ordered_comm_semiring (α : Type u_2) :
Type u_2

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 of this typeclass
Instances of other typeclasses for canonically_ordered_comm_semiring
  • canonically_ordered_comm_semiring.has_sizeof_inst
theorem mul_add_mul_le_mul_add_mul {α : Type u} [strict_ordered_semiring α] {a b c d : α} [has_exists_add_of_le α] (hab : a b) (hcd : c d) :
a * d + b * c a * c + b * d

Binary rearrangement inequality.

theorem mul_add_mul_le_mul_add_mul' {α : Type u} [strict_ordered_semiring α] {a b c d : α} [has_exists_add_of_le α] (hba : b a) (hdc : d c) :
a d + b c a c + b d

Binary rearrangement inequality.

theorem mul_add_mul_lt_mul_add_mul {α : Type u} [strict_ordered_semiring α] {a b c d : α} [has_exists_add_of_le α] (hab : a < b) (hcd : c < d) :
a * d + b * c < a * c + b * d

Binary strict rearrangement inequality.

theorem mul_add_mul_lt_mul_add_mul' {α : Type u} [strict_ordered_semiring α] {a b c d : α} [has_exists_add_of_le α] (hba : b < a) (hdc : d < c) :
a d + b c < a c + b d

Binary rearrangement inequality.

@[simp]
theorem canonically_ordered_comm_semiring.mul_pos {α : Type u} [canonically_ordered_comm_semiring α] {a b : α} :
0 < a * b 0 < a 0 < b
@[protected]
theorem add_le_cancellable.mul_tsub {α : Type u} [canonically_ordered_comm_semiring α] {a b c : α} [has_sub α] [has_ordered_sub α] [is_total α has_le.le] (h : add_le_cancellable (a * c)) :
a * (b - c) = a * b - a * c
@[protected]
theorem add_le_cancellable.tsub_mul {α : Type u} [canonically_ordered_comm_semiring α] {a b c : α} [has_sub α] [has_ordered_sub α] [is_total α has_le.le] (h : add_le_cancellable (b * c)) :
(a - b) * c = a * c - b * c
theorem mul_tsub {α : Type u} [canonically_ordered_comm_semiring α] [has_sub α] [has_ordered_sub α] [is_total α has_le.le] [contravariant_class α α has_add.add has_le.le] (a b c : α) :
a * (b - c) = a * b - a * c
theorem tsub_mul {α : Type u} [canonically_ordered_comm_semiring α] [has_sub α] [has_ordered_sub α] [is_total α has_le.le] [contravariant_class α α has_add.add has_le.le] (a b c : α) :
(a - b) * c = a * c - b * c