Zulip Chat Archive
Stream: mathlib4
Topic: rotation
vxctyxeha (May 05 2025 at 06:57):
how to solve this
import Mathlib
open Equiv Subgroup
theorem swapeq [NeZero n] (hn : 2 ≤ n): finRotate n 0=1 := by
```
Damiano Testa (May 05 2025 at 07:32):
I don't think that you need (hn : 2 ≤ n).
vxctyxeha (May 05 2025 at 10:12):
well i will try unfold finRotate
Last updated: Dec 20 2025 at 21:32 UTC