mul — Mathlib

English

If HasProd f a and HasProd g b hold (with respect to the same summation filter), then the product function h where h(x) = f(x)·g(x) has HasProd a·b.

Русский

Если выполнено HasProd f a и HasProd g b, то функция h, заданная h(x)=f(x)·g(x), имеет HasProd a·b.

LaTeX

$$HasProd (fun b => f b * g b) (a * b) L$$

Lean4

@[to_additive]
theorem mul (hf : HasProd f a L) (hg : HasProd g b L) : HasProd (fun b ↦ f b * g b) (a * b) L :=
  by
  dsimp only [HasProd] at hf hg ⊢
  simp_rw [prod_mul_distrib]
  exact hf.mul hg

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