smul_odd — Mathlib

English

Let f be even and g be odd, with a monoid action giving a • b in the codomain. Then the pointwise smul f • g is odd.

Русский

Пусть f чётна, а g нечётна; при этом имеется дейсвтие умножения по точке (f(a) • g(a)). Тогда f • g нечётна.

LaTeX

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

Lean4

theorem smul_odd [Monoid β] [AddGroup γ] [DistribMulAction β γ] (hf : f.Even) (hg : g.Odd) : (f • g).Odd :=
  by
  intro a
  simp only [Pi.smul_apply', hf a, hg a, smul_neg]

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