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
Methods
zero : M
-
Lean.Grind.AddCommMonoid M
add : M → M → M
-
Lean.Grind.AddCommMonoid M
add_zero : ∀ (a : M), a + 0 = a
-
Lean.Grind.AddCommMonoid M
add_comm : ∀ (a b : M), a + b = b + a
-
Lean.Grind.AddCommMonoid M
add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)
-
Lean.Grind.AddCommMonoid M
nsmul : HMul Nat M M
Scalar multiplication by natural numbers.
zero_nsmul : ∀ (a : M), 0 * a = 0
Scalar multiplication by zero is zero.
one_nsmul : ∀ (a : M), 1 * a = a
Scalar multiplication by one is the identity.
add_nsmul : ∀ (n m : Nat) (a : M), (n + m) * a = n * a + m * a
Scalar multiplication is distributive over addition in the natural numbers.
nsmul_zero : ∀ (n : Nat), n * 0 = 0
Scalar multiplication of zero is zero.
nsmul_add : ∀ (n : Nat) (a b : M), n * (a + b) = n * a + n * b
Scalar multiplication is distributive over addition in the module.