pmul_comm — Mathlib

English

The pointwise product is commutative when the codomain is a commutative monoid with zero: f.pmul g = g.pmul f.

Русский

Поэлементное произведение коммутативно, если кодом является коммутативный моноид с нулём: f.pmul g = g.pmul f.

LaTeX

$$$$ f\,\text{pmul}\, g = g\,\text{pmul}\, f $$$$

Lean4

theorem pmul_comm [CommMonoidWithZero R] (f g : ArithmeticFunction R) : f.pmul g = g.pmul f :=
  by
  ext
  simp [mul_comm]

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