Modules over ℕ and ℤ

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

Main definitions

• AddCommGroup.toNatModule: any AddCommMonoid is (uniquely) a module over the naturals. TODO: this name is not right!
• 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

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

Equations

• AddCommGroup.toNatModule = Module.mk ⋯ ⋯

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

Equations

• AddCommGroup.toIntModule M = Module.mk ⋯ ⋯

@[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

• Module.addCommMonoidToAddCommGroup R = AddCommGroup.mk ⋯

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.

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.

@[deprecated Nat.cast_smul_eq_nsmul]

theorem nsmul_eq_smul_cast (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.

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 AddCommMonoids should normally have exactly one ℕ-module structure by design.

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 := ⋯ }

theorem AddCommMonoid.nat_isScalarTower {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : IsScalarTower ℕ R M

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

theorem Nat.smul_one_eq_cast {R : Type u_5} [NonAssocSemiring R] (m : ℕ) : m • 1 = ↑m

theorem Int.smul_one_eq_cast {R : Type u_5} [NonAssocRing R] (m : ℤ) : m • 1 = ↑m

@[deprecated Nat.smul_one_eq_cast]

theorem Nat.smul_one_eq_coe {R : Type u_5} [NonAssocSemiring R] (m : ℕ) : m • 1 = ↑m

Alias of Nat.smul_one_eq_cast.

@[deprecated Int.smul_one_eq_cast]

theorem Int.smul_one_eq_coe {R : Type u_5} [NonAssocRing R] (m : ℤ) : m • 1 = ↑m

Alias of Int.smul_one_eq_cast.