smul_even

Mathlib.Algebra.Group.EvenFunction

URI: https://scilib.ai/kg/mathlib#Function.Odd.smul_even

← MathLib Explorer

English

If f is odd and g is even, then the pointwise smul f • g is odd.

Русский

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

LaTeX

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

Lean4

theorem smul_even [Ring β] [AddCommGroup γ] [Module β γ] (hf : f.Odd) (hg : g.Even) : (f • g).Odd :=
  by
  intro a
  simp only [Pi.smul_apply', hf a, hg a, neg_smul]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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