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

@[reducible, inline]

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

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 = match n, h, ⋯, ⋯ with | n.succ, h, h_mod, this => Module.mk ⋯ ⋯

@[reducible, inline]

abbrev 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_2 = AddCommGroup.toIntModule G
• AddCommGroup.zmodModule h_2 = AddCommMonoid.zmodModule h_2

@[reducible, inline]

abbrev QuotientAddGroup.zmodModule {n : ℕ} {G : Type u_3} [AddCommGroup G] {H : AddSubgroup G} (hH : ∀ (x : G), n • x ∈ H) : Module (ZMod n) (G ⧸ H)

The quotient of an abelian group by a subgroup containing all multiples of n is a n-torsion group.

Equations

• QuotientAddGroup.zmodModule hH = AddCommGroup.zmodModule ⋯

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

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

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.

See also: AddMonoidHom.toIntLinearMap, AddMonoidHom.toNatLinearMap, AddMonoidHom.toRatLinearMap

Equations

• AddMonoidHom.toZModLinearMap n f = { toFun := (↑f).toFun, map_add' := ⋯, map_smul' := ⋯ }

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 (toZModLinearMap n)

@[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₁) : ⇑(toZModLinearMap n f) = ⇑f

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.

See also: AddSubgroup.toIntSubmodule, AddSubmonoid.toNatSubmodule.

Equations

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

@[simp]

theorem AddSubgroup.toZModSubmodule_symm (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] : ⇑(toZModSubmodule n).symm = Submodule.toAddSubgroup

@[simp]

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

@[simp]

theorem AddSubgroup.mem_toZModSubmodule (n : ℕ) {M : Type u_1} [AddCommGroup M] [Module (ZMod n) M] {x : M} {S : AddSubgroup M} : x ∈ (toZModSubmodule n) S ↔ x ∈ S

@[simp]

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

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

theorem ZModModule.exists_submodule_subset_card_le {p : ℕ} {G : Type u_5} [AddCommGroup G] (hp : Nat.Prime p) [Module (ZMod p) G] (H : Submodule (ZMod p) G) {k : ℕ} (hk : k ≤ Nat.card ↥H) (h'k : k ≠ 0) : ∃ (H' : Submodule (ZMod p) G), Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H

In an elementary abelian p-group, every finite subgroup H contains a further subgroup of cardinality between k and p * k, if k ≤ |H|.