# Modules over `ℕ` and `ℤ` #

This file concerns modules where the scalars are the natural numbers or the integers.

## Main definitions #

- `AddCommMonoid.toNatModule`: any `AddCommMonoid` is (uniquely) a module over the naturals.
- `AddCommGroup.toIntModule`: any `AddCommGroup` is a module over the integers.

## Main results #

- `AddCommMonoid.uniqueNatModule`: there is an unique `AddCommMonoid ℕ M` structure for any `M`

## Tags #

semimodule, module, vector space

source
instance AddCommMonoid.toNatModule {M : Type u_3} [AddCommMonoid M] :
Module ℕ M
Equations

- AddCommMonoid.toNatModule = { toSMul := AddMonoid.toNatSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

source
instance AddCommGroup.toIntModule (M : Type u_3) [AddCommGroup M] :
Module ℤ M
Equations

- AddCommGroup.toIntModule M = { toSMul := SubNegMonoid.toZSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

source
@[reducible, inline]
abbrev Module.addCommMonoidToAddCommGroup (R : Type u_1) {M : Type u_3} [Ring R] [AddCommMonoid M] [Module R M] :
AddCommGroup M

An `AddCommMonoid` that is a `Module` over a `Ring` carries a natural `AddCommGroup` structure. See note [reducible non-instances].

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Nat.cast_smul_eq_nsmul (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (b : M) :
↑n • b = n • b

`nsmul` is equal to any other module structure via a cast.

source
theorem ofNat_smul_eq_nsmul (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (n : ℕ) [n.AtLeastTwo] (b : M) :
OfNat.ofNat n • b = OfNat.ofNat n • b

`nsmul` is equal to any other module structure via a cast.

source
theorem nat_smul_eq_nsmul {M : Type u_3} [AddCommMonoid M] (h : Module ℕ M) (n : ℕ) (x : M) :
SMul.smul n x = n • x

Convert back any exotic `ℕ`-smul to the canonical instance. This should not be needed since in mathlib all `AddCommMonoid`s should normally have exactly one `ℕ`-module structure by design.

source
def AddCommMonoid.uniqueNatModule {M : Type u_3} [AddCommMonoid M] :
Unique (Module ℕ M)

All `ℕ`-module structures are equal. Not an instance since in mathlib all `AddCommMonoid` should normally have exactly one `ℕ`-module structure by design.

Equations

- AddCommMonoid.uniqueNatModule = { default := inferInstance, uniq := ⋯ }

Instances For

source
instance AddCommMonoid.subsingletonNatModule {M : Type u_3} [AddCommMonoid M] :
Subsingleton (Module ℕ M)

All `ℕ`-module structures are equal. See also `AddCommMoniod.uniqueNatModule`.

source
instance AddCommMonoid.nat_isScalarTower {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
IsScalarTower ℕ R M
source
theorem map_natCast_smul {M : Type u_3} {M₂ : Type u_4} [AddCommMonoid M] [AddCommMonoid M₂] {F : Type u_5} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [Semiring R] [Semiring S] [Module R M] [Module S M₂] (x : ℕ) (a : M) :
f (↑x • a) = ↑x • f a
source
theorem Nat.smul_one_eq_cast {R : Type u_5} [NonAssocSemiring R] (m : ℕ) :
m • 1 = ↑m
source
theorem Int.smul_one_eq_cast {R : Type u_5} [NonAssocRing R] (m : ℤ) :
m • 1 = ↑m
source
theorem Int.cast_smul_eq_zsmul (R : Type u_1) {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (n : ℤ) (b : M) :
↑n • b = n • b

`zsmul` is equal to any other module structure via a cast.

source
theorem int_smul_eq_zsmul {M : Type u_3} [AddCommGroup M] (h : Module ℤ M) (n : ℤ) (x : M) :
SMul.smul n x = n • x

Convert back any exotic `ℤ`-smul to the canonical instance. This should not be needed since in mathlib all `AddCommGroup`s should normally have exactly one `ℤ`-module structure by design.

source
def AddCommGroup.uniqueIntModule {M : Type u_3} [AddCommGroup M] :
Unique (Module ℤ M)

All `ℤ`-module structures are equal. Not an instance since in mathlib all `AddCommGroup` should normally have exactly one `ℤ`-module structure by design.

Equations

- AddCommGroup.uniqueIntModule = { default := inferInstance, uniq := ⋯ }

Instances For

source
instance AddCommMonoid.subsingletonIntModule {M : Type u_3} [AddCommMonoid M] :
Subsingleton (Module ℤ M)

All `ℤ`-module structures are equal. See also `AddCommGroup.uniqueIntModule`.

source
theorem map_intCast_smul {M : Type u_3} {M₂ : Type u_4} [AddCommGroup M] [AddCommGroup M₂] {F : Type u_5} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [Ring R] [Ring S] [Module R M] [Module S M₂] (x : ℤ) (a : M) :
f (↑x • a) = ↑x • f a
source
instance AddCommGroup.intIsScalarTower {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] :
IsScalarTower ℤ R M