How to prove that in a cyclic group, an element satisfying a

Stream: new members

[Aina Sahalim]

I've formalized this in Lean (see below), but need help completing the proof:

theorem cyclic_subgroup_element {G : Type*} [group G] [is_cyclic G]
  (H : subgroup G) [fintype H] (n : ℕ) (hH : fintype.card H = n)
  (a : G) (ha : a ^ n = 1) : a ∈ H :=
sorry

I thought it would be a theorem in the mathlib, but I failed to find it. Can you provide a close thm to me or tell me how to proof:sob:

[Kevin Buzzard]

This doesn't compile. Are you sure you're using lean 4?

[Aina Sahalim]

sorry but what I actually want to proof is the sorry of the code below

theorem finite_field_power_iff {F : Type*} {k : ℕ} [Field F] [Fintype F] [DecidableEq F] {a : Fˣ}:
  (∃ x : Fˣ, x ^ k = a) ↔ a ^ ((Fintype.card F - 1) / (Nat.gcd (Fintype.card F - 1) k)) = 1 := by
  let m := Fintype.card F - 1
  let d := Nat.gcd m k
  let G := Fˣ
  haveI : IsCyclic G := instIsCyclicUnitsOfFinite
  have hd : d ∣ m := Nat.gcd_dvd_left m k
  let n := m / d
  have hn : n ∣ m := by
    rw [← Nat.mul_div_cancel' hd]
    exact dvd_mul_left n d
  have hgen : ∃ g : G, ∀ x, x ∈ zpowers g := IsCyclic.exists_generator
  rcases hgen with ⟨g, hg⟩
  have order_g : orderOf g = m := by
    rw [orderOf_eq_card_of_forall_mem_zpowers hg]
    rw [Nat.card_eq_fintype_card]
    rw [Fintype.card_units]
  let b := g ^ k
  have order_b : orderOf b = n := by
    rw [orderOf_pow, order_g]
  let H := zpowers b
  have card_H : Fintype.card H = n := by
    rw [Fintype.card_zpowers]
    exact order_b
  have mem_H_iff_power : a ∈ H ↔ ∃ x : G, x ^ k = a := by
    constructor
    · intro ha
      rw [mem_zpowers_iff] at ha
      obtain ⟨j, hj⟩ := ha
      use g ^ j
      rw [← hj]
      unfold b
      group
    · rintro ⟨x, rfl⟩
      obtain ⟨j, hj⟩ := hg x
      rw [← hj]
      group
      rw [mul_comm]
      rw [zpow_mul]
      simp only [zpow_natCast]
      use j
  rw [← mem_H_iff_power]
  have : a ∈ H ↔ a ^ n = 1 := by
    sorry
  rw [this]

I try to simplyfy the problem but I failed. I am using lean 4 for sure . Would you do me a favor?

[Aina Sahalim]

The natural language of the problem is "How to prove that in a cyclic group, an element satisfying a^n=1 must belong to a finite subgroup of order n?" and the lean code is

theorem cyclic_subgroup_element {G : Type*} [Group G] [IsCyclic G]
    (H : Subgroup G) [Fintype H] (n : ℕ) (hH : Fintype.card H = n)
    (a : G) (ha : a ^ n = 1) : a ∈ H :=
  sorry

[Aaron Liu]

What you have actually stated is "in every cyclic group, every element satisfying a ^ n = 1 must belong to every finite subgroup of order n", and this is false.

[Aaron Liu]

To get an exists statement, you need an existential quantifier.

[Yaël Dillies]

Aaron Liu said:

What you have actually stated is "in every cyclic group, every element satisfying a ^ n = 1 must belong to every finite subgroup of order n", and this is false.

What's a counterexample?

[Aaron Liu]

Oh I thought I had a counterexample but HMMMM I must have lost it

[Aaron Liu]

Ok maybe it's true

[Aaron Liu]

But you have still written a different theorem, and I think the original statement is actually the false one since you can set n = 0 and get an empty subgroup.

[Aaron Liu]

I'll just pretend I was referring to the informal statement all along

[Yaël Dillies]

What if you replace the informal statement by "How to prove that in a cyclic group, an element satisfying a^n=1 must belong to a given finite subgroup of order n?"? I feel like you simply misread the informal statement

[Aaron Liu]

really?

[Aaron Liu]

maybe

[Aaron Liu]

I guess that's the problem with natural language, sometimes it can be misinterpreted