NYLL
Module

PrimePowerCharacters.lean

Nyll.ProCGroups.Abelian.PrimePowerCharacters
2 declarations indexed from sourceView source ↗

Module documentation

Prime-power characters separate abelian pro-p groups

Imports4
Imported by4

Declarations

theorem

exists_primePower_character_finite

L20 ↗
ProCGroups.Abelian.exists_primePower_character_finite
Documentation

A nonidentity element of a finite abelian p-group is detected by a character to a cyclic p-power group.

Source context 2 commands

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

namespace ProCGroups.Abelian
universe u
Lean source · statement
theorem exists_primePower_character_finite
    {p : ℕ} [Fact p.Prime]
    {A : Type u} [CommGroup A] [Finite A]
    (hA : IsPGroup p A) {x : A} (hx : x ≠ 1) :
    ∃ n : ℕ, 0 < n ∧ ∃ χ : A →* Multiplicative (ZMod (p ^ n)), χ x ≠ 1
theorem

exists_primePower_character_proP

L59 ↗
ProCGroups.Abelian.exists_primePower_character_proP
Documentation

Continuous cyclic p-power characters separate a Hausdorff abelian pro-p group.

Source context 2 commands

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

namespace ProCGroups.Abelian
universe u
Lean source · statement
theorem exists_primePower_character_proP
    {p : ℕ} [Fact p.Prime]
    {A : Type u} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]
    [T2Space A]
    (hA : ProC.HasOpenNormalBasisInClass (FiniteGroupClass.pGroup p) A)
    {x : A} (hx : x ≠ 1) :
    ∃ n : ℕ, 0 < n ∧ ∃ χ : A →ₜ* Multiplicative (ZMod (p ^ n)), χ x ≠ 1

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