English
If two elements x,y have the same order in a finite left-cancellative monoid, there exists an equivalence between the submonoids generated by x and by y mapping x^i to y^i.
Русский
Если два элемента x,y имеют одинаковый порядок в конечном левою отменяемом моноиде, существует эквивалентность между подмоноидами, порождаемыми x и y, отображающая x^i в y^i.
LaTeX
$$powersEquivPowers : (orderOf x = orderOf y) → powers x ≃ powers y$$
Lean4
/-- The equivalence between `Submonoid.powers` of two elements `x, y` of the same order, mapping
`x ^ i` to `y ^ i`. -/
@[to_additive /-- The equivalence between `Submonoid.multiples` of two elements `a, b` of the same additive
order, mapping `i • a` to `i • b`. -/
]
noncomputable def powersEquivPowers (h : orderOf x = orderOf y) : powers x ≃ powers y :=
(finEquivPowers <| isOfFinOrder_of_finite _).symm.trans <|
(finCongr h).trans <| finEquivPowers <| isOfFinOrder_of_finite _
