mathlib3

59eef0a2 - refactor(algebra/periodic): weaken another `antiperiodic` typeclass assumption (#15961)

refactor(algebra/periodic): weaken another `antiperiodic` typeclass assumption (#15961) Followup to #15941 and #15782, weakening the typeclass assumption on the codomain of the antiperiodic function in `antiperiodic.const_sub` (added by #15782) in the same way as done for other lemmas in #15941.