const_smul

Mathlib.Algebra.Group.EvenFunction

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

English

Multiplying a function by a constant preserves evenness.

Русский

Умножение функции на константу сохраняет чётность.

LaTeX

$$$\\forall a, r \\cdot g(-a) = r \\cdot g(a).$$$

Lean4

theorem const_smul [SMul β γ] (hg : g.Even) (r : β) : (r • g).Even :=
  by
  intro a
  simp only [Pi.smul_apply, hg a]

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

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

Разделы

Аффилиация

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