Theorems · Theorem · real analysis

Function.Antiperiodic.periodic

∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → Function.Periodic f (2 • c)

If a function is antiperiodic with antiperiod c, then it is also Periodic with period 2 • c.

Defined in

Mathlib.Algebra.Ring.Periodic

Cited by

3 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound

Assumes

AddMonoidInvolutiveNeg