Commit 2025-10-28 10:18 0f086d10

View on Github →

chore(Data/Nat/Periodic): golf (#30970)

Estimated changes

Modified Mathlib/Data/Nat/Periodic.lean

modified theorem Nat.periodic_coprime

modified theorem Nat.periodic_gcd

modified theorem Nat.periodic_mod