The `ZMod n`-module structure on Abelian groups whose elements have order dividing `n` #

@[reducible]

def AddCommMonoid.zmodModule {n : ℕ} {M : Type u_1} [NeZero n] [AddCommMonoid M] (h : ∀ (x : M), n • x = 0) :

The ZMod n-module structure on commutative monoids whose elements have order dividing n ≠ 0. Also implies a group structure via Module.addCommMonoidToAddCommGroup. See note [reducible non-instances].

Equations

AddCommMonoid.zmodModule h = let_fun h_mod := ⋯; let_fun this := ⋯; match n, h, h_mod, this with | n.succ, h, h_mod, this => Module.mk ⋯ ⋯

Instances For

source

@[reducible]

def AddCommGroup.zmodModule {n : ℕ} {G : Type u_3} [AddCommGroup G] (h : ∀ (x : G), n • x = 0) :

Module (ZMod n) G

The ZMod n-module structure on Abelian groups whose elements have order dividing n. See note [reducible non-instances].

Equations

AddCommGroup.zmodModule h = match n, h with | 0, h => AddCommGroup.intModule G | n.succ, h => AddCommMonoid.zmodModule h

Instances For

source

theorem ZMod.map_smul {n : ℕ} {M : Type u_1} {M₁ : Type u_2} {F : Type u_3} [AddCommGroup M] [AddCommGroup M₁] [FunLike F M M₁] [AddMonoidHomClass F M M₁] [Module (ZMod n) M] [Module (ZMod n) M₁] (f : F) (c : ZMod n) (x : M) :

f (c • x) = c • f x

source

theorem ZMod.smul_mem {n : ℕ} {M : Type u_1} {S : Type u_4} [AddCommGroup M] [Module (ZMod n) M] [SetLike S M] [AddSubgroupClass S M] {x : M} {K : S} (hx : x ∈ K) (c : ZMod n) :

c • x ∈ K

source

def AddMonoidHom.toZModLinearMap (n : ℕ) {M : Type u_1} {M₁ : Type u_2} [AddCommGroup M] [AddCommGroup M₁] [Module (ZMod n) M] [Module (ZMod n) M₁] (f : M →+ M₁) :

M →ₗ[ZMod n] M₁

Reinterpret an additive homomorphism as a ℤ/nℤ-linear map.

Equations

AddMonoidHom.toZModLinearMap n f = { toFun := f.toFun, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

theorem AddMonoidHom.toZModLinearMap_injective (n : ℕ) {M : Type u_1} {M₁ : Type u_2} [AddCommGroup M] [AddCommGroup M₁] [Module (ZMod n) M] [Module (ZMod n) M₁] :

Function.Injective (AddMonoidHom.toZModLinearMap n)

source

@[simp]

theorem AddMonoidHom.coe_toZModLinearMap (n : ℕ) {M : Type u_1} {M₁ : Type u_2} [AddCommGroup M] [AddCommGroup M₁] [Module (ZMod n) M] [Module (ZMod n) M₁] (f : M →+ M₁) :

⇑(AddMonoidHom.toZModLinearMap n f) = ⇑f

source

def AddSubgroup.toZModSubmodule (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] :

AddSubgroup M ≃o Submodule (ZMod n) M

Reinterpret an additive subgroup of a ℤ/nℤ-module as a ℤ/nℤ-submodule.

Equations

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

Instances For

source

@[simp]

theorem AddSubgroup.toZModSubmodule_symm (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] :

⇑(AddSubgroup.toZModSubmodule n).symm = Submodule.toAddSubgroup

source

@[simp]

theorem AddSubgroup.coe_toZModSubmodule (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] (S : AddSubgroup M) :

↑((AddSubgroup.toZModSubmodule n) S) = ↑S

source

@[simp]

theorem AddSubgroup.toZModSubmodule_toAddSubgroup (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] (S : AddSubgroup M) :

((AddSubgroup.toZModSubmodule n) S).toAddSubgroup = S

source

@[simp]

theorem Submodule.toAddSubgroup_toZModSubmodule (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] (S : Submodule (ZMod n) M) :

(AddSubgroup.toZModSubmodule n) S.toAddSubgroup = S

Documentation

Mathlib.Data.ZMod.Module

The `ZMod n`-module structure on Abelian groups whose elements have order dividing `n` #

The ZMod n-module structure on Abelian groups whose elements have order dividing n #

The `ZMod n`-module structure on Abelian groups whose elements have order dividing `n` #