Specific Groups

Results named in Tau Ceti's TauCeti.GroupTheory.SpecificGroups modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremEuler's product formula for the elements of order divisible by f#

For f dividing the order h of a cyclic group, the elements of order divisible by f are a proportion ∏ p ∣ f, (1 - p ^ -(v_p h - v_p f + 1)) of the group, the product running over the primes of f.

IsCyclic.card_filter_dvd_orderOf_eq_mul_prod_primeFactors.{u_1} {α : Type u_1} [Group α] [Fintype α]
  [IsCyclic α] {f : ℕ} (hf : f ∣ Fintype.card α) :
  ↑{τ | f ∣ orderOf τ}.card =
    ↑(Fintype.card α) *
      ∏ p ∈ f.primeFactors,
        (1 - (↑p ^ ((Fintype.card α).factorization p - f.factorization p + 1))⁻¹)

Lean

Formalized in Tau Ceti as IsCyclic.card_filter_dvd_orderOf_eq_mul_prod_primeFactors.

Other forms

Euler's product formula for the elements of additive order divisible by f. Formalized in Tau Ceti as IsAddCyclic.card_filter_dvd_addOrderOf_eq_add_sum_primeFactors.

IsAddCyclic.card_filter_dvd_addOrderOf_eq_add_sum_primeFactors.{u_1} {α : Type u_1} [AddGroup α]
  [Fintype α] [IsAddCyclic α] {f : ℕ} (hf : f ∣ Fintype.card α) :
  ↑{τ | f ∣ addOrderOf τ}.card =
    ↑(Fintype.card α) *
      ∏ p ∈ f.primeFactors,
        (1 - (↑p ^ ((Fintype.card α).factorization p - f.factorization p + 1))⁻¹)

Sources

• Tau Ceti documentation: IsCyclic.card_filter_dvd_orderOf_eq_mul_prod_primeFactors
• Source of IsCyclic.card_filter_dvd_orderOf_eq_mul_prod_primeFactors in TauCeti/GroupTheory/SpecificGroups/Cyclic/OrderCount.lean

LeanIsCyclic.card_filter_dvd_orderOf_eq_mul_prod_primeFactors · IsAddCyclic.card_filter_dvd_addOrderOf_eq_add_sum_primeFactors

Used by 1

Used byThe crossing constant approaches 1 / #Aut_K(L)

TheoremThe finite-field generation theorem#

every Steinberg fixed point over the generator field is a product of the standard generators. A fixed point fixing ∞ is a torus element times a unipotent generator, and any other is carried to one by w u(a, b) for the unipotent generator moving its last column onto the line through e₀.

TauCeti.SuzukiLieIndex.finiteFixedSubgroup_le_suzukiGroup (m : ℕ)
  (hvalid : (TauCeti.LieTypeIndex.suzuki m).Valid) :
  TauCeti.SuzukiLieIndex.finiteFixedSubgroup m hvalid ≤ TauCeti.suzukiGroup m

Lean

Formalized in Tau Ceti as TauCeti.SuzukiLieIndex.finiteFixedSubgroup_le_suzukiGroup.

Sources

• Tau Ceti documentation: TauCeti.SuzukiLieIndex.finiteFixedSubgroup_le_suzukiGroup
• Source of TauCeti.SuzukiLieIndex.finiteFixedSubgroup_le_suzukiGroup in TauCeti/GroupTheory/SpecificGroups/CFSG/Suzuki/Generation.lean

LeanTauCeti.SuzukiLieIndex.finiteFixedSubgroup_le_suzukiGroup

Uses 1 · Used by 1

Proof usesCauchy--Binet for 2 × 2 minors

Used byThe rank-one Bruhat decomposition Sz(q) = B ∪ B w B, for m ≠ 0

TheoremThe rank-one Bruhat decomposition Sz(q) = B ∪ B w B, for m ≠ 0#

TauCeti.Suzuki.mem_borelSubgroupOf_or_mem_doubleCoset (m : ℕ) (hm : m ≠ 0)
  (g : ↥(TauCeti.suzukiGroup m)) :
  g ∈ TauCeti.Suzuki.borelSubgroupOf m ∨
    g ∈
      DoubleCoset.doubleCoset (TauCeti.Suzuki.weylOf m) ↑(TauCeti.Suzuki.borelSubgroupOf m)
        ↑(TauCeti.Suzuki.borelSubgroupOf m)

Lean

Formalized in Tau Ceti as TauCeti.Suzuki.mem_borelSubgroupOf_or_mem_doubleCoset.

Sources

• Tau Ceti documentation: TauCeti.Suzuki.mem_borelSubgroupOf_or_mem_doubleCoset
• Source of TauCeti.Suzuki.mem_borelSubgroupOf_or_mem_doubleCoset in TauCeti/GroupTheory/SpecificGroups/CFSG/Suzuki/Simple.lean

LeanTauCeti.Suzuki.mem_borelSubgroupOf_or_mem_doubleCoset

Uses 2

Proof usesCauchy--Binet for 2 × 2 minors · The finite-field generation theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.