mul — Mathlib

English

If f and g are both Multipliable with respect to L, then their pointwise product is Multipliable with respect to L.

Русский

Если f и g обе Multipliable по отношению к L, то их покомпонентное произведение тоже Multipliable по отношению к L.

LaTeX

$$Multipliable (fun b => f b * g b) L$$

Lean4

@[to_additive]
theorem mul (hf : Multipliable f L) (hg : Multipliable g L) : Multipliable (fun b ↦ f b * g b) L :=
  (hf.hasProd.mul hg.hasProd).multipliable

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