pmul_apply

Mathlib.NumberTheory.ArithmeticFunction

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.pmul_apply

English

The pointwise product pmul of arithmetic functions satisfies (f pmul g)(x) = f(x) g(x).

Русский

Поэлементное произведение арифметических функций удовлетворяет (f pmul g)(x) = f(x) g(x).

LaTeX

$$$$ (f \text{ pmul } g)(x) = f(x) \cdot g(x) $$$$

Lean4

@[simp]
theorem pmul_apply [MulZeroClass R] {f g : ArithmeticFunction R} {x : ℕ} : f.pmul g x = f x * g x :=
  rfl

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

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

Разделы

Аффилиация

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