A question about dihedral groups

Stream: new members

[well]

This is my problem . Let n≥3 and k∈Zn​. Prove that in Dn​, have
$r^ks=sr^(n−k)$.
For the dihedral group, I am not sure how to approach it based on the most basic definition. My thought is $D_n = \{ r^n = s^2 = 1 | s * r * s = r^(-1)\ }$.
Where r represents rotation and n represents reflection. If I can define it this way, the problem will be very simple.
I have just started learning Lean and I'm not very proficient with it yet. Please help me solve this problem. Thank you very much.

[Eric Wieser]

Are you aware of docs#DihedralGroup ?

[Eric Wieser]

Also, please use #backticks for code or $$dollars$$ to write math, so that it doesn't turn into italics!

[well]

This is my problem . Let $n≥3$ and $k∈Z_n$​. Prove that in $D_n$​, have
$r^k*s=s*r^{(n−k)}$.
For the dihedral group, I am not sure how to approach it based on the most basic definition. My thought is $D_n$ = $\{$ $r^n = s^2 = 1 | s * r * s = r^{-1}$ $\}$.
Where r represents rotation and n represents reflection. If I can define it this way, the problem will be very simple.
I have just started learning Lean and I'm not very proficient with it yet. Please help me solve this problem. Thank you very much.

[Ruben Van de Velde]

Double dollars (you can edit your message)

[well]

This is my problem . Let $n≥3$ and $k∈Z_n$​. Prove that in $D_n$​, have
$r^k*s=s*r^{(n−k)}$.
For the dihedral group, I am not sure how to approach it based on the most basic definition. My thought is $D_n$ = $\{$ $r^n = s^2 = 1 | s * r * s = r^{-1}$ $\}$.
Where r represents rotation and n represents reflection. If I can define it this way, the problem will be very simple.
I have just started learning Lean and I'm not very proficient with it yet. Please help me solve this problem. Thank you very much.

[Eric Wieser]

Eric Wieser said:

Are you aware of docs#DihedralGroup ?

Did you see this message?