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

• AddCommMonoid M

Methods

zero : M

add : M → 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)

nsmul : SMul Nat M

zero_nsmul : ∀ (a : M), 0 • a = 0

add_one_nsmul : ∀ (n : Nat) (a : M), (n + 1) • a = n • a + a

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

• AddCommGroup M

Methods

zero : M

add : M → 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)

neg : M → M

sub : M → M → M

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

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

nsmul : SMul Nat M

zsmul : SMul Int M

zero_zsmul : ∀ (a : M), 0 • a = 0

one_zsmul : ∀ (a : M), 1 • a = a

add_zsmul : ∀ (n m : Int) (a : M), (n + m) • a = n • a + m • a

zsmul_natCast_eq_nsmul : ∀ (n : Nat) (a : M), ↑n • a = n • 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

• 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