map_mul_of_coprime

Mathlib.NumberTheory.ArithmeticFunction

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.IsMultiplicative.map_mul_of_coprime

← MathLib Explorer

English

If gcd(m,n)=1 and f is multiplicative, then f(mn)=f(m)f(n).

Русский

Если gcd(m,n)=1 и f — мультипликативна, то f(mn)=f(m)f(n).

LaTeX

$$$f(mn)=f(m)\,f(n)$$$

Lean4

@[simp]
theorem map_mul_of_coprime {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {m n : ℕ} (h : m.gcd n = 1) :
    f (m * n) = f m * f n :=
  hf.2 h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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