div — Mathlib

English

If hf and hg are antiperiodic with the same shift c, then the quotient f / g is periodic with shift c.

Русский

Если f и g антиперодичны с одним и тем же сдвигом c, то f / g периодичен сдвигом c.

LaTeX

$$$\forall x,\ \frac{f(x + c)}{g(x + c)} = \frac{f(x)}{g(x)}$$$

Lean4

theorem div [Add α] [DivisionMonoid β] [HasDistribNeg β] (hf : Antiperiodic f c) (hg : Antiperiodic g c) :
    Periodic (f / g) c := by simp_all [neg_div_neg_eq]

Похожие утверждения