English
There exists g ∈ G with orderOf g = exponent G.
Русский
Существует элемент g ∈ G, чьей экспоненте равен экспонента G.
LaTeX
$$$\\\\exists g : G, \\\\operatorname{orderOf} g = \\\\operatorname{exponent} G$$$
Lean4
@[to_additive]
theorem exists_orderOf_eq_exponent (hG : ExponentExists G) : ∃ g : G, orderOf g = exponent G :=
by
have he := hG.exponent_ne_zero
have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩
have hfin : (Set.range (orderOf : G → ℕ)).Finite := by
rwa [← exponent_ne_zero_iff_range_orderOf_finite hG.orderOf_pos]
obtain ⟨t, ht⟩ := hne.csSup_mem hfin
use t
apply Nat.dvd_antisymm (order_dvd_exponent _)
refine Nat.dvd_of_primeFactorsList_subperm he ?_
rw [List.subperm_ext_iff]
by_contra! h
obtain ⟨p, hp, hpe⟩ := h
replace hp := Nat.prime_of_mem_primeFactorsList hp
simp only [Nat.primeFactorsList_count_eq] at hpe
set k := (orderOf t).factorization p with hk
obtain ⟨g, hg⟩ := hp.exists_orderOf_eq_pow_factorization_exponent G
suffices orderOf t < orderOf (t ^ p ^ k * g) by
rw [ht] at this
exact this.not_ge (le_csSup hfin.bddAbove <| Set.mem_range_self _)
have hpk : p ^ k ∣ orderOf t := Nat.ordProj_dvd _ _
have hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k := by
rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt hpe
have hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g) :=
by
rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
nth_rw 1 [← pow_one p]
have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 :=
by
rw [hpk', Nat.factorization_div hpk]
simp [k, hp]
rw [this]
-- Porting note: convert made to_additive complain
exact Nat.pow_succ_factorization_not_dvd (hG.orderOf_pos <| t ^ p ^ k).ne' hp
rw [(Commute.all _ g).orderOf_mul_eq_mul_orderOf_of_coprime hcoprime, hpk', hg, ha, hk, pow_add, pow_add, pow_one, ←
mul_assoc, ← mul_assoc, Nat.div_mul_cancel, mul_assoc, lt_mul_iff_one_lt_right <| hG.orderOf_pos t, ← pow_succ]
· exact one_lt_pow₀ hp.one_lt a.succ_ne_zero
· exact hpk
