mul — Mathlib

English

If f and g are periodic with the same period c, then their product f*g is periodic with period c.

Русский

Если f и g периодичны с тем же периодом c, то их произведение f*g периодично с периодом c.

LaTeX

$$$\forall f,g:\alpha\to\beta,\ \mathrm{Periodic}(f,c)\land \mathrm{Periodic}(g,c)\Rightarrow \mathrm{Periodic}(f*g,c).$$$

Lean4

@[to_additive]
protected theorem mul [Add α] [Mul β] (hf : Periodic f c) (hg : Periodic g c) : Periodic (f * g) c := by simp_all

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