English
Equivalence between zpowers of x and y for same order extends to Subgroup.zpowers equality.
Русский
Эквивалентность zpowers x и zpowers y для одинакового порядка распространяется на равенство zpowers.
LaTeX
$$zpowersEquivZPowers (h : orderOf x = orderOf y) : Subgroup.zpowers x ≃ Subgroup.zpowers y$$
Lean4
/-- The equivalence between `Subgroup.zpowers` of two elements `x, y` of the same order, mapping
`x ^ i` to `y ^ i`. -/
@[to_additive /-- The equivalence between `Subgroup.zmultiples` of two elements `a, b` of the same additive
order, mapping `i • a` to `i • b`. -/
]
noncomputable def zpowersEquivZPowers (h : orderOf x = orderOf y) : Subgroup.zpowers x ≃ Subgroup.zpowers y :=
(finEquivZPowers <| isOfFinOrder_of_finite _).symm.trans <|
(finCongr h).trans <| finEquivZPowers <| isOfFinOrder_of_finite _
