NYLL
Module

PrimaryDetection.lean

Nyll.ProCGroups.Abelian.PrimaryDetection
1 declaration indexed from sourceView source ↗

Module documentation

Primary quotients separate profinite abelian groups

Imports4
Imported by3

Declarations

theorem

eq_one_of_forall_primaryQuotient

L19 ↗
ProCGroups.ProC.eq_one_of_forall_primaryQuotient
Source context 2 commands

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

namespace ProCGroups.ProC
universe u
Lean source · statement
theorem eq_one_of_forall_primaryQuotient
    {A : Type u} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]
    [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
    (a : A)
    (ha : ∀ (p : ℕ) [Fact p.Prime],
      QuotientGroup.mk' (proCResidualCore (FiniteGroupClass.pGroup p) A) a = 1) :
    a = 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.