proving two zpowers are equal

Stream: general

[Frederick Pu]

Is there anything in mathlib proving the following statement about cyclic subgroups?

hy'x : y ∈ Subgroup.zpowers x
this : orderOf x = orderOf y
⊢ Subgroup.zpowers y = Subgroup.zpowers x

[Kenny Lau]

$(x,y \in \Bbb Q^\times) = (2,4)$

[Frederick Pu]

for finite groups i mean

[Frederick Pu]

so Subgroup.zpowers x and Subgroup.zpowers y are isomorphic

[Frederick Pu]

and you know that y must go to x or x^-1

[Kenny Lau]

Frederick Pu said:

and you know that y must go to x or x^-1

$(x, y \in (\Bbb Z/11)^\times) = (2, 4)$

[Aaron Liu]

I think the statement is still true (for finite groups) but it's definitely not that simple

[Frederick Pu]

i think it's just double inclusion

[Aaron Liu]

x could be any n-th power of y for n coprime to the order of x and y

[Frederick Pu]

since y \in zpowers x, zpowers y \subseteq zpowers x

[Frederick Pu]

so use the lemma that if H \subseteq K and |H| = |K| then H = K for finite groups

[Kenny Lau]

great, now you have a proof

[Frederick Pu]

but is it in mathlib tho

[Frederick Pu]

i feel like it would be convenient

[Aaron Liu]

I don't see it in my searches but you can use the proof you have and prove it yourself

[Frederick Pu]

:(

[Frederick Pu]

my assignments due in like 5 hours i think ill just accept that it's true lol

[Aaron Liu]

Surely it won't take five whole hours for such a simple proof?

[Frederick Pu]

i mean i have other parts of my main proof i havent finished yet

[Aaron Liu]

here you can have this

import Mathlib

example {G : Type*} [Group G] [Finite G] {x y : G}
    (hy'x : y ∈ Subgroup.zpowers x)
    (this : orderOf x = orderOf y) :
    Subgroup.zpowers y = Subgroup.zpowers x := by
  refine SetLike.coe_injective (Set.eq_of_subset_of_ncard_le ?_ (le_of_eq ?_))
  · simpa using hy'x
  · rw [Set.ncard_eq_toFinset_card, Set.ncard_eq_toFinset_card]
    apply Finset.card_eq_of_equiv
    simpa using zpowersEquivZPowers this

[Frederick Pu]

also what about smth like this?

this✝ : Subgroup.zpowers x < ⊤
this : Subgroup.zpowers x ≠ ⊥
⊢ ∃ y, y ∉ Subgroup.zpowers x

[Ruben Van de Velde]

docs#SetLike.exists_not_mem_of_ne_top ?

[Frederick Pu]

hmm im not 4.25 but i cant find that one

[Ruben Van de Velde]

Yeah, I believe it's pretty new. You can copy it, though

[Ruben Van de Velde]

docs#Set.ne_univ_iff_exists_notMem is the essential element

[Aaron Liu]

Ruben Van de Velde said:

docs#SetLike.exists_not_mem_of_ne_top ?

Didn't we switch over to calling it notMem a while ago