mul_even

Mathlib.Algebra.Group.EvenFunction

URI: https://scilib.ai/kg/mathlib#Function.Even.mul_even

English

If f and g are even, then their pointwise product f * g is even.

Русский

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

LaTeX

$$$\\forall a, f(-a) = f(a) \\wedge g(-a) = g(a) \\Rightarrow (f * g)(-a) = (f * g)(a).$$$

Lean4

theorem mul_even (hf : f.Even) (hg : g.Even) : (f * g).Even :=
  by
  intro a
  simp only [Pi.mul_apply, hf a, hg a]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru