mathlib

b64b1f88 - feat(algebra/periodic): generalize some lemmas (#18334)

feat(algebra/periodic): generalize some lemmas (#18334) * Drop some commutativity assumptions. * Golf some proofs. * Add `protected` here and there for future compatibility with Lean 4.