class Wheel (α : Type u) extends AddCommMonoid α, CommMonoid α : Type u

A Wheel is an algebraic structure which has two binary operations (+,*), like a ring. Similarly to a commutative ring, a Wheel is a commutative monoid in both operations. Additionally, there is a multiplicative unary map wDiv which is an involution, as well as a few idiosyncratic properties in the interactions of the +,* and wDiv.

• 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
• mul : α → α → α
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• npow : ℕ → α → α
• npow_zero (x : α) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• mul_comm (a b : α) : a * b = b * a
• wDiv (a : α) : α
• inv_wDiv (a : α) : \ₐ\ₐa = a
• mul_wDiv (a b : α) : \ₐ(a * b) = \ₐa * \ₐb
• add_wDiv (a b c : α) : (a + b * c) * \ₐb = a * \ₐb + c + 0 * b
• left_mul_distrib (a b c : α) : (a + b) * c + 0 * c = a * c + b * c
• left_mul_distrib' (a b c : α) : (a + 0 * b) * c = a * c + 0 * b
• zero_mul_zero : 0 * 0 = 0
• div_add_zero (a b : α) : \ₐ(a + 0 * b) = \ₐa + 0 * b
• wDiv_zero_add (a : α) : 0 * \ₐ0 + a = 0 * \ₐ0

def «term\ₐ_» : Lean.ParserDescr

Equations

• «term\ₐ_» = Lean.ParserDescr.node `«term\ₐ_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "\\ₐ") (Lean.ParserDescr.cat `term 100))

@[simp]

theorem Wheel.wdiv_one {α : Type u} [Wheel α] : \ₐ1 = 1

We have that wDiv 1 is one, in general

@[simp]

theorem Wheel.zero_mul_add {α : Type u} [Wheel α] (a b : α) : 0 * a + 0 * b = 0 * a * b

For any two terms a b :α with [Wheel α] , we have that 0*a + 0*b = 0*a*b.

@[simp]

theorem Wheel.zero_wdiv_mul {α : Type u} [Wheel α] (a : α) : 0 * \ₐ0 * a = 0 * \ₐ0

For any a :α and [Wheel α] , (0* \ₐ 0)*a = 0* \ₐ 0. Morally, this is like saying infinity times anything is infinity, complementing the axiom wDiv_zero_add.

@[simp]

theorem Wheel.wdiv_self {α : Type u} [Wheel α] (a : α) : a * \ₐa = 1 + 0 * (a * \ₐa)

For any a :α and [Wheel α] , a*\ₐa = 1 + 0*(a*\ₐa) .

theorem Wheel.wdiv_right_cancel' {α : Type u} [Wheel α] (a b c : α) : a * c = b * c → a + 0 * c * \ₐc = b + 0 * c * \ₐc

For any a b c :α and [Wheel α] , a*c = b*c → a + 0*c*\ₐc = b + 0*c*\ₐc. This is the version of cancellation that wheels enjoy.

theorem Wheel.isUnit_add_eq_div_add {α : Type u} [Wheel α] (c : α) (hc : IsUnit c) : ∃ (b : α), c * b = 1 ∧ b * c = 1 ∧ b + 0 * \ₐc = \ₐc + 0 * b

If c :α is a unit and [Wheel α] , then the inverse and Wheel self-division are related