Module

ElementaryAbelianRank.lean

Nyll.ProCGroups.ProP.ElementaryAbelianRank

2 declarations indexed from sourceView source ↗

Module documentation

Generator bounds for finite elementary abelian groups

This file compares bounded topological generation of a finite discrete commutative group with the dimension of a supplied ZMod p-module structure on its additive copy. It creates no group or module instance: the canonical structure for a power--commutator quotient is installed only in the importing pro-p leaf.

Imports6

Mathlib.Algebra.Field.ZMod
Mathlib.Algebra.Module.ZMod
Mathlib.LinearAlgebra.Basis.VectorSpace
Mathlib.LinearAlgebra.Dimension.Constructions
Mathlib.RingTheory.Finiteness.Cardinality
Nyll.ProCGroups.FiniteGeneration.Basic

Imported by3

theorem

finrank_le_of_topologicallyGeneratedByAtMost_zmod

L34 ↗

ClassFieldTower.ProP.finrank_le_of_topologicallyGeneratedByAtMost_zmod

Documentation

A finite topological generating set of a discrete ZMod p-module bounds its dimension.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open Set
namespace ClassFieldTower.ProP
universe u
open ProCGroups.Generation
open ProCGroups.FiniteGeneration

Lean source · statement

theorem finrank_le_of_topologicallyGeneratedByAtMost_zmod
    {p : ℕ} {Q : Type u} [Fact (Nat.Prime p)]
    [TopologicalSpace Q] [CommGroup Q] [IsTopologicalGroup Q] [DiscreteTopology Q]
    [Module (ZMod p) (Additive Q)] {d : ℕ}
    (hgen : TopologicallyGeneratedByAtMost d Q) :
    Module.finrank (ZMod p) (Additive Q) ≤ d

theorem

topologicallyGeneratedByAtMost_finrank_zmod

L87 ↗

ClassFieldTower.ProP.topologicallyGeneratedByAtMost_finrank_zmod