pdiv_apply

Mathlib.NumberTheory.ArithmeticFunction

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

English

For any f,g in ArithmeticFunction with values in a semiring, pdiv f g (n) = f(n) / g(n).

Русский

Для любых функций f,g из ArithmeticFunction, значения в полугруппе, pdiv f g (n) = f(n) / g(n).

LaTeX

$$$$ pdiv f g n = f n / g n $$$$

Lean4

@[simp]
theorem pdiv_apply [GroupWithZero R] (f g : ArithmeticFunction R) (n : ℕ) : pdiv f g n = f n / g n :=
  rfl

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

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

Разделы

Аффилиация

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