If G is a rank d free ℤ-module, then G/nG is a finite group of cardinality n ^ d.

@[reducible, inline]

abbrev modN (G : Type u_1) [AddCommGroup G] (n : ℕ) : Type u_1

modN G n denotes the quotient of G by multiples of n

Equations

• modN G n = (G ⧸ LinearMap.range ((LinearMap.lsmul ℤ G) ↑n))

instance instModuleZModModN {G : Type u_1} [AddCommGroup G] {n : ℕ} : Module (ZMod n) (modN G n)

Equations

• instModuleZModModN = QuotientAddGroup.zmodModule ⋯

noncomputable def modNBasis {G : Type u_1} [AddCommGroup G] [Module.Free ℤ G] {n : ℕ} [NeZero n] : Basis (Module.Free.ChooseBasisIndex ℤ G) (ZMod n) (modN G n)

Given a free module G over ℤ, construct the corresponding basis of G / ⟨n⟩ over ℤ / nℤ.

Equations

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

instance modN.instModuleFinite {G : Type u_1} [AddCommGroup G] [Module.Free ℤ G] {n : ℕ} [NeZero n] [Module.Finite ℤ G] : Module.Finite (ZMod n) (modN G n)

Equations

• ⋯ = ⋯

instance modN.instFinite {G : Type u_1} [AddCommGroup G] [Module.Free ℤ G] {n : ℕ} [NeZero n] [Module.Finite ℤ G] : Finite (modN G n)

Equations

• ⋯ = ⋯

@[simp]

theorem card_modN (G : Type u_1) [AddCommGroup G] [Module.Free ℤ G] (n : ℕ) [NeZero n] [Module.Finite ℤ G] : Nat.card (modN G n) = n ^ Module.finrank ℤ G