A module over the natural numbers, i.e. a type with zero, addition, and scalar multiplication by natural numbers, satisfying appropriate compatibilities.

Equivalently, an additive commutative monoid.

Use IntModule if the type has negation.

Instance Constructor

Lean.Grind.NatModule.mk.{u}

Extends

• Zero M
• Add M
• HMul Nat M M

Methods

zero : M

add : M → M → M

hMul : Nat → M → M

add_zero : ∀ (a : M), a + 0 = a

add_comm : ∀ (a b : M), a + b = b + a

add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)

zero_hmul : ∀ (a : M), 0 * a = 0

one_hmul : ∀ (a : M), 1 * a = a

add_hmul : ∀ (n m : Nat) (a : M), (n + m) * a = n * a + m * a

hmul_zero : ∀ (n : Nat), n * 0 = 0

hmul_add : ∀ (n : Nat) (a b : M), n * (a + b) = n * a + n * b

A module over the integers, i.e. a type with zero, addition, negation, subtraction, and scalar multiplication by integers, satisfying appropriate compatibilities.

Equivalently, an additive commutative group.

Instance Constructor

Lean.Grind.IntModule.mk.{u}

Extends

• Zero M
• Add M
• Neg M
• Sub M

Methods

zero : M

add : M → M → M

neg : M → M

sub : M → M → M

hmulNat : HMul Nat M M

hmulInt : HMul Int M M

add_zero : ∀ (a : M), a + 0 = a

add_comm : ∀ (a b : M), a + b = b + a

add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)

zero_hmul : ∀ (a : M), 0 * a = 0

one_hmul : ∀ (a : M), 1 * a = a

add_hmul : ∀ (n m : Int) (a : M), (n + m) * a = n * a + m * a

hmul_zero : ∀ (n : Int), n * 0 = 0

hmul_add : ∀ (n : Int) (a b : M), n * (a + b) = n * a + n * b

neg_add_cancel : ∀ (a : M), -a + a = 0

sub_eq_add_neg : ∀ (a b : M), a - b = a + -b

hmul_nat : ∀ (n : Nat) (a : M), ↑n * a = n * a

A preorder is a reflexive, transitive relation ≤ with a < b defined in the obvious way.

Instance Constructor

Lean.Grind.Preorder.mk.{u}

Extends

• LE α
• LT α

Methods

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

A partial order is a preorder with the additional property that a ≤ b and b ≤ a implies a = b.

Instance Constructor

Lean.Grind.PartialOrder.mk.{u}

Extends

• Lean.Grind.Preorder α

Methods

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

le_antisymm : ∀ {a b : α}, a ≤ b → b ≤ a → a = b

A linear order is a partial order with the additional property that every pair of elements is comparable.

Instance Constructor

Lean.Grind.LinearOrder.mk.{u}

Extends

• Lean.Grind.PartialOrder α

Methods

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

le_antisymm : ∀ {a b : α}, a ≤ b → b ≤ a → a = b

le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

Addition is compatible with a preorder if a ≤ b ↔ a + c ≤ b + c.

Instance Constructor

Lean.Grind.OrderedAdd.mk.{u}

Methods

add_le_left_iff : ∀ {a b : M} (c : M), a ≤ b ↔ a + c ≤ b + c

A ring which is also equipped with a preorder is considered a strict ordered ring if addition, negation, and multiplication are compatible with the preorder, and 0 < 1.

Instance Constructor

Lean.Grind.OrderedRing.mk.{u}

Extends

• Lean.Grind.OrderedAdd R

Methods

add_le_left_iff : ∀ {a b : R} (c : R), a ≤ b ↔ a + c ≤ b + c

zero_lt_one : 0 < 1

mul_lt_mul_of_pos_left : ∀ {a b c : R}, a < b → 0 < c → c * a < c * b

mul_lt_mul_of_pos_right : ∀ {a b c : R}, a < b → 0 < c → a * c < b * c