Theorems · Theorem · real analysis

Function.Antiperiodic.const_sub

∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (a : α), Function.Antiperiodic (fun x => f (a - x)) c

Defined in

Mathlib.Algebra.Ring.Periodic

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext

Assumes

AddCommGroupInvolutiveNeg