NYLL
Module

StandardClasses.lean

Nyll.ProCGroups.FiniteGroups.StandardClasses
58 declarations indexed from sourceView source ↗

Module documentation

Standard classes of finite groups

This module constructs the cyclic, abelian, solvable, nilpotent, finite \(p\)-group, \(\sigma\)-group, and bounded-exponent abelian classes. It proves the subgroup, quotient, product, extension, formation, and full-formation properties needed later, together with the finite-order arithmetic and cyclic witnesses supporting those proofs.

Imports3
Imported by40

Declarations

theorem

exists_factorization_lt_of_not_dvd

L27 ↗
ProCGroups.FiniteGroupClass.exists_factorization_lt_of_not_dvd
Documentation

If \(a \nmid b\), then some prime factor has a larger exponent in \(a\) than in \(b\).

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem exists_factorization_lt_of_not_dvd
    {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (hndvd : ¬ a ∣ b) :
    ∃ p, b.factorization p < a.factorization p
theorem

nat_factorization_le_self_of_prime

L38 ↗
ProCGroups.FiniteGroupClass.nat_factorization_le_self_of_prime
Documentation

The p-adic exponent of a positive integer is at most the integer itself.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem nat_factorization_le_self_of_prime
    {A p : ℕ} (hp : Nat.Prime p) :
    A.factorization p ≤ A
theorem

gcd_mul_dvd_pow_depth

L44 ↗
ProCGroups.FiniteGroupClass.gcd_mul_dvd_pow_depth
Documentation

The depth \((K*d)^(A+1)\) is large enough for the GCD-conditioned cyclic reduction.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem gcd_mul_dvd_pow_depth
    {K d A : ℕ} (hK : 0 < K) (hd : 0 < d) (hA : 0 < A) :
    Nat.gcd (d * A) (K * (K * d) ^ (A + 1)) ∣ (K * d) ^ (A + 1)
def

cyclic

L110 ↗
ProCGroups.FiniteGroupClass.cyclic
Documentation

The class of finite cyclic groups.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · full declaration
def cyclic : FiniteGroupClass.{u} where
  pred := fun G [_] => Finite G ∧ IsCyclic G
  finite_of_mem := fun hG => hG.1
  mem_of_mulEquiv := by
    intro G H _ _ e hG
    let : Finite G := hG.1
    exact ⟨Finite.of_equiv G e.toEquiv, e.isCyclic.mp hG.2⟩
def

abelian

L119 ↗
ProCGroups.FiniteGroupClass.abelian
Documentation

The class of finite abelian groups.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · full declaration
def abelian : FiniteGroupClass.{u} where
  pred := fun G [_] => Finite G ∧ ∀ a b : G, a * b = b * a
  finite_of_mem := fun hG => hG.1
  mem_of_mulEquiv := by
    intro G H _ _ e hG
    let : Finite G := hG.1
    refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
    intro a b
    apply e.symm.injective
    simpa using hG.2 (e.symm a) (e.symm b)
def

solvable

L131 ↗
ProCGroups.FiniteGroupClass.solvable
Documentation

The class of finite solvable groups.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · full declaration
def solvable : FiniteGroupClass.{u} where
  pred := fun G [_] => Finite G ∧ Group.IsSolvable G
  finite_of_mem := fun hG => hG.1
  mem_of_mulEquiv := by
    intro G H _ _ e hG
    let : Finite G := hG.1
    let : Group.IsSolvable G := hG.2
    exact ⟨Finite.of_equiv G e.toEquiv,
      Group.isSolvable_of_surjective (f := e.toMonoidHom) e.surjective⟩
def

nilpotent

L142 ↗
ProCGroups.FiniteGroupClass.nilpotent
Documentation

The finite group class consisting of finite nilpotent groups.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · full declaration
def nilpotent : FiniteGroupClass.{u} where
  pred := fun G [_] => Finite G ∧ Group.IsNilpotent G
  finite_of_mem := fun hG => hG.1
  mem_of_mulEquiv := by
    intro G H _ _ e hG
    let : Finite G := hG.1
    exact ⟨Finite.of_equiv G e.toEquiv,
      (Group.isNilpotent_congr e).mp hG.2⟩
def

pGroup

L152 ↗
ProCGroups.FiniteGroupClass.pGroup
Documentation

The class of finite \(p\)-groups.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · full declaration
def pGroup (p : ℕ) [Fact (Nat.Prime p)] : FiniteGroupClass.{u} where
  pred := fun G [_] => Finite G ∧ IsPGroup p G
  finite_of_mem := fun hG => hG.1
  mem_of_mulEquiv := by
    intro G H _ _ e hG
    let : Finite G := hG.1
    exact ⟨Finite.of_equiv G e.toEquiv,
      hG.2.of_surjective e.toMonoidHom e.surjective⟩
def

IsSigmaNumber

L165 ↗
ProCGroups.FiniteGroupClass.IsSigmaNumber
Documentation

A natural number whose prime divisors all lie in \(\Sigma\). This is the finite-level condition underlying finite \(\Sigma\)-groups and pro-\(\Sigma\) groups.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
def IsSigmaNumber (sigma : Set ℕ) (n : ℕ) : Prop
theorem

of_dvd

L171 ↗
ProCGroups.FiniteGroupClass.IsSigmaNumber.of_dvd
Documentation

Every divisor of a \(\Sigma\)-number is again a \(\Sigma\)-number.

Source context 4 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
namespace IsSigmaNumber
Lean source · statement
theorem of_dvd {sigma : Set ℕ} {m n : ℕ} (hn : IsSigmaNumber sigma n) (hmn : m ∣ n) :
    IsSigmaNumber sigma m
theorem

mul

L177 ↗
ProCGroups.FiniteGroupClass.IsSigmaNumber.mul
Documentation

The product of two \(\Sigma\)-numbers is a \(\Sigma\)-number.

Source context 4 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
namespace IsSigmaNumber
Lean source · statement
theorem mul {sigma : Set ℕ} {m n : ℕ} (hm : IsSigmaNumber sigma m)
    (hn : IsSigmaNumber sigma n) :
    IsSigmaNumber sigma (m * n)
theorem

prod

L184 ↗
ProCGroups.FiniteGroupClass.IsSigmaNumber.prod
Documentation

A finite product of \(\Sigma\)-numbers is a \(\Sigma\)-number.

Source context 4 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
namespace IsSigmaNumber
Lean source · statement
theorem prod {sigma : Set ℕ} {ι : Type*} (s : Finset ι) (f : ι → ℕ)
    (hf : ∀ i ∈ s, IsSigmaNumber sigma (f i)) :
    IsSigmaNumber sigma (s.prod f)
theorem

pow

L199 ↗
ProCGroups.FiniteGroupClass.IsSigmaNumber.pow
Documentation

A natural-number power of a \(\Sigma\)-number is a \(\Sigma\)-number.

Source context 4 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
namespace IsSigmaNumber
Lean source · statement
theorem pow {sigma : Set ℕ} {n k : ℕ} (hn : IsSigmaNumber sigma n) :
    IsSigmaNumber sigma (n ^ k)
theorem

prime_pow_of_mem

L210 ↗
ProCGroups.FiniteGroupClass.IsSigmaNumber.prime_pow_of_mem
Documentation

A prime power whose prime lies in \(\Sigma\) is a \(\Sigma\)-number.

Source context 4 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
namespace IsSigmaNumber
Lean source · statement
theorem prime_pow_of_mem {sigma : Set ℕ} {p k : ℕ}
    (hpsigma : p ∈ sigma) (hp : Nat.Prime p) :
    IsSigmaNumber sigma (p ^ k)
def

sigmaGroup

L227 ↗
ProCGroups.FiniteGroupClass.sigmaGroup
Documentation

The class of finite \(\Sigma\)-groups: finite groups whose order has no prime divisors outside \(\Sigma\).

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · full declaration
def sigmaGroup (sigma : Set ℕ) : FiniteGroupClass.{u} where
  pred := fun G [_] => Finite G ∧ IsSigmaNumber sigma (Nat.card G)
  finite_of_mem := fun hG => hG.1
  mem_of_mulEquiv := by
    intro G H _ _ e hG
    let : Finite G := hG.1
    refine ⟨Finite.of_equiv G e.toEquiv, ?_⟩
    simpa [Nat.card_congr e.toEquiv] using hG.2
def

abelianExponent

L237 ↗
ProCGroups.FiniteGroupClass.abelianExponent
Documentation

The class of finite abelian groups of exponent dividing \(n\).

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · full declaration
def abelianExponent (n : ℕ) : FiniteGroupClass.{u} where
  pred := fun G [_] =>
    Finite G ∧ (∀ a b : G, a * b = b * a) ∧ ∀ g : G, g ^ n = 1
  finite_of_mem := fun hG => hG.1
  mem_of_mulEquiv := by
    intro G H _ _ e hG
    let : Finite G := hG.1
    refine ⟨Finite.of_equiv G e.toEquiv, ?_, ?_⟩
    · intro a b
      apply e.symm.injective
      simpa using hG.2.1 (e.symm a) (e.symm b)
    · intro g
      apply e.symm.injective
      simpa using hG.2.2 (e.symm g)
theorem

isPGroup_pi

L257 ↗
ProCGroups.FiniteGroupClass.isPGroup_pi
Documentation

Finite products of abstract \(p\)-groups are \(p\)-groups.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {p : ℕ}
Lean source · statement
theorem isPGroup_pi {ι : Type u} [Finite ι] {G : ι → Type v}
    [∀ i, Group (G i)] (hG : ∀ i, IsPGroup p (G i)) :
    IsPGroup p ((i : ι) → G i)
theorem

pGroup_formation

L277 ↗
ProCGroups.FiniteGroupClass.pGroup_formation
Documentation

The class of finite \(p\)-groups is a formation.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {p : ℕ}
Lean source · statement
theorem pGroup_formation (p : ℕ) [Fact (Nat.Prime p)] :
    FiniteGroupClass.Formation (FiniteGroupClass.pGroup p)
instance

pGroup_containsTrivialQuotients

L290 ↗
ProCGroups.FiniteGroupClass.pGroup_containsTrivialQuotients
Documentation

Finite \(p\)-groups contain the trivial quotients.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {p : ℕ}
Lean source · statement
instance pGroup_containsTrivialQuotients (p : ℕ) [Fact (Nat.Prime p)] :
    ContainsTrivialQuotients (pGroup p : FiniteGroupClass.{u})
theorem

pGroup_subgroupClosed

L295 ↗
ProCGroups.FiniteGroupClass.pGroup_subgroupClosed
Documentation

Subgroups of finite \(p\)-groups are finite \(p\)-groups.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {p : ℕ}
Lean source · statement
theorem pGroup_subgroupClosed (p : ℕ) [Fact (Nat.Prime p)] : SubgroupClosed (pGroup p)
theorem

finite_of_finite_normalSubgroup_and_quotient

L301 ↗
ProCGroups.FiniteGroupClass.finite_of_finite_normalSubgroup_and_quotient
Documentation

A group is finite when a normal subgroup and the corresponding quotient are finite.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {p : ℕ}
Lean source · statement
theorem finite_of_finite_normalSubgroup_and_quotient
    {E : Type u} [Group E] (N : Subgroup E) [N.Normal]
    [Finite N] [Finite (E ⧸ N)] :
    Finite E
theorem

pGroup_extensionClosed

L322 ↗
ProCGroups.FiniteGroupClass.pGroup_extensionClosed
Documentation

Extensions of finite \(p\)-groups are finite \(p\)-groups.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {p : ℕ}
Lean source · statement
theorem pGroup_extensionClosed (p : ℕ) [Fact (Nat.Prime p)] :
    ExtensionClosed (pGroup p)
theorem

pGroup_hereditary

L345 ↗
ProCGroups.FiniteGroupClass.pGroup_hereditary
Documentation

The class of finite \(p\)-groups is hereditary under subgroups.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {p : ℕ}
Lean source · statement
theorem pGroup_hereditary (p : ℕ) [Fact (Nat.Prime p)] : Hereditary (pGroup p)
theorem

sigmaGroup_isomClosed

L357 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_isomClosed
Documentation

sigmaGroup is closed under group isomorphism.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem sigmaGroup_isomClosed (sigma : Set ℕ) : IsomClosed (sigmaGroup sigma)
theorem

sigmaGroup_subgroupClosed

L365 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_subgroupClosed
Documentation

sigmaGroup is closed under subgroups.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem sigmaGroup_subgroupClosed (sigma : Set ℕ) : SubgroupClosed (sigmaGroup sigma)
theorem

sigmaGroup_quotientClosed

L372 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_quotientClosed
Documentation

sigmaGroup is closed under quotients.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem sigmaGroup_quotientClosed (sigma : Set ℕ) : QuotientClosed (sigmaGroup sigma)
theorem

sigmaGroup_finiteProductClosed

L380 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_finiteProductClosed
Documentation

sigmaGroup is closed under finite products.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem sigmaGroup_finiteProductClosed (sigma : Set ℕ) : FiniteProductClosed (sigmaGroup sigma)
theorem

sigmaGroup_variety

L391 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_variety
Documentation

sigmaGroup is a finite-group variety.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem sigmaGroup_variety (sigma : Set ℕ) : Variety (sigmaGroup sigma)
theorem

sigmaGroup_formation

L396 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_formation
Documentation

sigmaGroup is a formation of finite groups.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem sigmaGroup_formation (sigma : Set ℕ) : Formation (sigmaGroup sigma)
theorem

sigmaGroup_extensionClosed

L400 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_extensionClosed
Documentation

Finite Σ-groups are closed under extensions.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem sigmaGroup_extensionClosed (sigma : Set ℕ) :
    ExtensionClosed (sigmaGroup sigma)
theorem

sigmaGroup_melnikovFormation

L414 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_melnikovFormation
Documentation

Finite Σ-groups form a Melnikov formation.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · full declaration
theorem sigmaGroup_melnikovFormation (sigma : Set ℕ) :
    MelnikovFormation (sigmaGroup sigma) where
  formation := sigmaGroup_formation sigma
  normalSubgroupClosed := fun N _ hG => sigmaGroup_subgroupClosed sigma N hG
  extensionClosed := sigmaGroup_extensionClosed sigma
theorem

sigmaGroup_fullFormation

L421 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_fullFormation
Documentation

Finite Σ-groups form a full formation.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · full declaration
theorem sigmaGroup_fullFormation (sigma : Set ℕ) :
    FullFormation (sigmaGroup sigma) where
  melnikovFormation := sigmaGroup_melnikovFormation sigma
  subgroupClosed := sigmaGroup_subgroupClosed sigma
theorem

sigmaGroup_cyclicZMod

L427 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_cyclicZMod
Documentation

A positive Σ-number gives an allowed finite cyclic Σ-group.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem sigmaGroup_cyclicZMod
    {sigma : Set ℕ} {n : ℕ} (hn : 0 < n)
    (hsigma : IsSigmaNumber sigma n) :
    sigmaGroup sigma (ULift.{u} (Multiplicative (ZMod n)))
theorem

sigmaGroup_nontrivialCyclic

L443 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_nontrivialCyclic
Documentation

A nonempty set of primes supplies a nontrivial finite cyclic Σ-group.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem sigmaGroup_nontrivialCyclic
    {sigma : Set ℕ} (hsigma : ∃ p, p ∈ sigma ∧ Nat.Prime p) :
    ∃ (A : Type u) (_ : Group A) (_ : Finite A),
      sigmaGroup sigma A ∧ IsCyclic A ∧ Nontrivial A
theorem

sigmaGroup_prod_multiplicativeZMod

L461 ↗
ProCGroups.FiniteGroupClass.sigmaGroup_prod_multiplicativeZMod
Documentation

Product of a finite Σ-group with the concrete cyclic group ZMod N.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem sigmaGroup_prod_multiplicativeZMod
    {sigma : Set ℕ} {Q : Type u} [Group Q]
    (hQ : sigmaGroup sigma Q)
    {N : ℕ} (hNpos : 0 < N)
    (hNsigma : IsSigmaNumber sigma N) :
    sigmaGroup sigma (Q × Multiplicative (ZMod N))
theorem

exists_prime_power_orderOf_gt_padicValNat_of_zpow_ne_one

L478 ↗
ProCGroups.FiniteGroupClass.exists_prime_power_orderOf_gt_padicValNat_of_zpow_ne_one
Documentation

A nontrivial finite Σ-group power supplies a coefficient prime and depth.

Source context 5 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
section
variable {sigma : Set ℕ}
Lean source · statement
theorem exists_prime_power_orderOf_gt_padicValNat_of_zpow_ne_one
    {sigma : Set ℕ} {G : Type u} [Group G] [Finite G]
    (hG : sigmaGroup sigma G) {g : G} {n : ℤ} (hgn : g ^ n ≠ 1) :
    ∃ ℓ σ : ℕ,
      Nat.Prime ℓ ∧ 0 < σ ∧ ℓ ∈ sigma ∧
        padicValNat ℓ n.natAbs < σ ∧ ℓ ^ σ ∣ orderOf g
theorem

abelian_subgroupClosed

L534 ↗
ProCGroups.FiniteGroupClass.abelian_subgroupClosed
Documentation

Finite abelian groups are closed under subgroups.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelian_subgroupClosed : SubgroupClosed abelian
theorem

abelian_quotientClosed

L542 ↗
ProCGroups.FiniteGroupClass.abelian_quotientClosed
Documentation

Finite abelian groups are closed under quotients.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelian_quotientClosed : QuotientClosed abelian
theorem

abelian_finiteProductClosed

L555 ↗
ProCGroups.FiniteGroupClass.abelian_finiteProductClosed
Documentation

Finite abelian groups are closed under finite direct products.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelian_finiteProductClosed : FiniteProductClosed abelian
theorem

abelian_variety

L566 ↗
ProCGroups.FiniteGroupClass.abelian_variety
Documentation

Finite abelian groups form a variety.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelian_variety : Variety abelian
theorem

abelian_isomClosed

L571 ↗
ProCGroups.FiniteGroupClass.abelian_isomClosed
Documentation

Finite abelian groups are closed under isomorphism.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelian_isomClosed : IsomClosed abelian
theorem

abelian_formation

L581 ↗
ProCGroups.FiniteGroupClass.abelian_formation
Documentation

Finite abelian groups form a formation.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelian_formation : Formation abelian
theorem

abelianExponent_subgroupClosed

L585 ↗
ProCGroups.FiniteGroupClass.abelianExponent_subgroupClosed
Documentation

Subgroups of finite abelian groups of bounded exponent again have bounded exponent.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelianExponent_subgroupClosed (n : ℕ) : SubgroupClosed (abelianExponent n)
theorem

abelianExponent_quotientClosed

L597 ↗
ProCGroups.FiniteGroupClass.abelianExponent_quotientClosed
Documentation

Quotients of finite abelian groups of bounded exponent again have bounded exponent.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelianExponent_quotientClosed (n : ℕ) : QuotientClosed (abelianExponent n)
theorem

abelianExponent_finiteProductClosed

L610 ↗
ProCGroups.FiniteGroupClass.abelianExponent_finiteProductClosed
Documentation

Finite products of finite abelian groups of bounded exponent again have bounded exponent.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelianExponent_finiteProductClosed (n : ℕ) :
    FiniteProductClosed (abelianExponent n)
theorem

abelianExponent_variety

L624 ↗
ProCGroups.FiniteGroupClass.abelianExponent_variety
Documentation

abelianExponent is a finite-group variety.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelianExponent_variety (n : ℕ) : Variety (abelianExponent n)
theorem

abelianExponent_isomClosed

L629 ↗
ProCGroups.FiniteGroupClass.abelianExponent_isomClosed
Documentation

Finite abelian groups of exponent dividing \(n\) are closed under isomorphism.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelianExponent_isomClosed (n : ℕ) : IsomClosed (abelianExponent n)
theorem

abelianExponent_formation

L642 ↗
ProCGroups.FiniteGroupClass.abelianExponent_formation
Documentation

Finite abelian groups of exponent dividing \(n\) form a formation.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem abelianExponent_formation (n : ℕ) : Formation (abelianExponent n)
theorem

cyclic_isomClosed

L646 ↗
ProCGroups.FiniteGroupClass.cyclic_isomClosed
Documentation

Finite cyclic groups are closed under isomorphism.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem cyclic_isomClosed : IsomClosed cyclic
theorem

cyclic_quotientClosed

L654 ↗
ProCGroups.FiniteGroupClass.cyclic_quotientClosed
Documentation

Finite cyclic groups are closed under quotients.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem cyclic_quotientClosed : QuotientClosed cyclic
theorem

solvable_isomClosed

L662 ↗
ProCGroups.FiniteGroupClass.solvable_isomClosed
Documentation

Finite solvable groups are closed under isomorphism.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem solvable_isomClosed : IsomClosed solvable
theorem

solvable_quotientClosed

L670 ↗
ProCGroups.FiniteGroupClass.solvable_quotientClosed
Documentation

Finite solvable groups are closed under quotients.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem solvable_quotientClosed : QuotientClosed solvable
theorem

nilpotent_isomClosed

L678 ↗
ProCGroups.FiniteGroupClass.nilpotent_isomClosed
Documentation

Finite nilpotent groups are closed under isomorphism.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem nilpotent_isomClosed : IsomClosed nilpotent
theorem

nilpotent_quotientClosed

L686 ↗
ProCGroups.FiniteGroupClass.nilpotent_quotientClosed
Documentation

Finite nilpotent groups are closed under quotients.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem nilpotent_quotientClosed : QuotientClosed nilpotent
theorem

cyclic_to_nilpotent

L694 ↗
ProCGroups.FiniteGroupClass.cyclic_to_nilpotent
Documentation

Every finite cyclic group is finite nilpotent.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem cyclic_to_nilpotent {G : Type u} [Group G] :
    cyclic G → nilpotent G
theorem

cyclic_to_solvable

L702 ↗
ProCGroups.FiniteGroupClass.cyclic_to_solvable
Documentation

Every finite cyclic group belongs to the finite solvable class.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem cyclic_to_solvable {G : Type u} [Group G] :
    cyclic G → solvable G
theorem

pGroup_to_nilpotent

L709 ↗
ProCGroups.FiniteGroupClass.pGroup_to_nilpotent
Documentation

Every finite \(p\)-group belongs to the finite nilpotent class.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem pGroup_to_nilpotent {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] :
    pGroup p G → nilpotent G
theorem

pGroup_to_solvable

L715 ↗
ProCGroups.FiniteGroupClass.pGroup_to_solvable
Documentation

Every finite \(p\)-group belongs to the finite solvable class.

Source context 3 commands

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

namespace ProCGroups
universe u v
namespace FiniteGroupClass
Lean source · statement
theorem pGroup_to_solvable {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] :
    pGroup p G → solvable G

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