Finite horizontal quotients are p-groups

Proved

HorizontalPadicL.horizontalFiniteGroup_isPGroup

by davidloeffler · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryp-adic-l-functionsp-groups

Every finite horizontal quotient, being a finite product of additive groups Z/p^{m_i}Z, is a finite p-group.

Preamble

import Definitions.Def_KN_SeededThetaConstruction
import Mathlib.GroupTheory.PGroup

set_option autoImplicit false
noncomputable section
open scoped BigOperators

Formal statement

namespace HorizontalPadicL

/-- Every finite horizontal quotient is a finite `p`-group. -/
theorem horizontalFiniteGroup_isPGroup
    {p : ℕ} [Fact p.Prime] (m : ℕ → ℕ) (A : Finset ℕ) :
    IsPGroup p (HorizontalFiniteGroup p m A) := by sorry

end HorizontalPadicL

Source

Elementary finite abelian group theory.

View graph