English
For a prime p, there exists an element g in G with orderOf g = p^{(exponent G).factorization p}.
Русский
Пусть p — простое число. Существует элемент g в G такой, что orderOf(g) = p^{(exponent G).factorization p}.
LaTeX
$$$\\\\exists g : G, \\\\operatorname{orderOf} g = p^{(\\\\operatorname{exponent} G).factorization p}$$$
Lean4
@[to_additive exists_addOrderOf_eq_pow_padic_val_nat_add_exponent]
theorem _root_.Nat.Prime.exists_orderOf_eq_pow_factorization_exponent {p : ℕ} (hp : p.Prime) :
∃ g : G, orderOf g = p ^ (exponent G).factorization p :=
by
haveI := Fact.mk hp
rcases eq_or_ne ((exponent G).factorization p) 0 with (h | h)
· refine ⟨1, by rw [h, pow_zero, orderOf_one]⟩
have he : 0 < exponent G :=
Ne.bot_lt fun ht => by
rw [ht] at h
apply h
rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
rw [← Finsupp.mem_support_iff] at h
obtain ⟨g, hg⟩ : ∃ g : G, g ^ (exponent G / p) ≠ 1 :=
by
suffices key : ¬exponent G ∣ exponent G / p by rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at key
exact fun hd =>
hp.one_lt.not_ge
((mul_le_iff_le_one_left he).mp <|
Nat.le_of_dvd he <| Nat.mul_dvd_of_dvd_div (Nat.dvd_of_mem_primeFactors h) hd)
obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := Nat.ordProj_dvd _ _
obtain ⟨t, ht⟩ := Nat.exists_eq_succ_of_ne_zero (Finsupp.mem_support_iff.mp h)
refine ⟨g ^ k, ?_⟩
rw [ht]
apply orderOf_eq_prime_pow
· rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
· rw [← Nat.succ_eq_add_one, ← ht, ← pow_mul, mul_comm, ← hk]
exact pow_exponent_eq_one g
