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.

canonically_ordered_comm_semiring
- canonically_ordered_add_monoid & multiplication & * respects ≤ & no zero divisors
- comm_semiring & a ≤ b ↔ ∃ c, b = a + c & no zero divisors

TODO #

We're still missing some typeclasses, like

canonically_ordered_semiring They have yet to come up in practice.

@[class]

structure canonically_ordered_comm_semiring (α : Type u_2) :

Type u_2

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 : α), canonically_ordered_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), canonically_ordered_comm_semiring.nsmul n.succ x = x + canonically_ordered_comm_semiring.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
bot : α
bot_le : ∀ (x : α), ⊥ ≤ x
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
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
nat_cast : ℕ → α
nat_cast_zero : canonically_ordered_comm_semiring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), canonically_ordered_comm_semiring.nat_cast (n + 1) = canonically_ordered_comm_semiring.nat_cast n + 1) . "control_laws_tac"
npow : ℕ → α → α
npow_zero' : (∀ (x : α), canonically_ordered_comm_semiring.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), canonically_ordered_comm_semiring.npow n.succ x = x * canonically_ordered_comm_semiring.npow n x) . "try_refl_tac"
mul_comm : ∀ (a b : α), a * b = b * a
eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : α}, a * b = 0 → a = 0 ∨ b = 0

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

@[instance]

def canonically_ordered_comm_semiring.to_comm_semiring (α : Type u_2) [self : canonically_ordered_comm_semiring α] :

comm_semiring α

@[instance]

def canonically_ordered_comm_semiring.to_canonically_ordered_add_monoid (α : Type u_2) [self : canonically_ordered_comm_semiring α] :

canonically_ordered_add_monoid α

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.

@[protected, instance]

def canonically_ordered_comm_semiring.to_no_zero_divisors {α : Type u} [canonically_ordered_comm_semiring α] :

no_zero_divisors α

@[protected, instance]

def canonically_ordered_comm_semiring.to_covariant_mul_le {α : Type u} [canonically_ordered_comm_semiring α] :

covariant_class α α has_mul.mul has_le.le

@[protected, instance]

def canonically_ordered_comm_semiring.to_ordered_comm_monoid {α : Type u} [canonically_ordered_comm_semiring α] :

ordered_comm_monoid α

Equations

canonically_ordered_comm_semiring.to_ordered_comm_monoid = {mul := canonically_ordered_comm_semiring.mul _inst_1, mul_assoc := _, one := canonically_ordered_comm_semiring.one _inst_1, one_mul := _, mul_one := _, npow := canonically_ordered_comm_semiring.npow _inst_1, npow_zero' := _, npow_succ' := _, mul_comm := _, le := canonically_ordered_comm_semiring.le _inst_1, lt := canonically_ordered_comm_semiring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _}

@[protected, instance]

def canonically_ordered_comm_semiring.to_ordered_comm_semiring {α : Type u} [canonically_ordered_comm_semiring α] :

ordered_comm_semiring α

Equations

canonically_ordered_comm_semiring.to_ordered_comm_semiring = {add := canonically_ordered_comm_semiring.add _inst_1, add_assoc := _, zero := canonically_ordered_comm_semiring.zero _inst_1, zero_add := _, add_zero := _, nsmul := canonically_ordered_comm_semiring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := canonically_ordered_comm_semiring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := canonically_ordered_comm_semiring.one _inst_1, one_mul := _, mul_one := _, nat_cast := canonically_ordered_comm_semiring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := canonically_ordered_comm_semiring.npow _inst_1, npow_zero' := _, npow_succ' := _, le := canonically_ordered_comm_semiring.le _inst_1, lt := canonically_ordered_comm_semiring.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_le_mul_of_nonneg_left := _, mul_le_mul_of_nonneg_right := _, mul_comm := _}

@[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