mul_odd

Mathlib.Algebra.Group.EvenFunction

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

English

If f is even and g is odd, then (f * g) is odd.

Русский

Если f чётна, а g нечётна, то f*g нечётна.

LaTeX

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

Lean4

theorem mul_odd [HasDistribNeg R] (hf : f.Even) (hg : g.Odd) : (f * g).Odd :=
  by
  intro a
  simp only [Pi.mul_apply, hf a, hg a, mul_neg]

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

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

Разделы

Аффилиация

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