map_gcd — Mathlib

English

For multiplicative f, f(x.gcd y) equals (f x · f y)/f(x·lcm y) when f(x·lcm y) ≠ 0.

Русский

Для мультипликативной f: f(gcd(x,y)) = f(x)f(y)/f(lcm(x,y)) при ненулевом знаменателе.

LaTeX

$$$f(x\gcd y) = \dfrac{f(x)f(y)}{f(x\mathrm{lcm} y)}$ при $f(x\mathrm{lcm} y)\neq 0$$$

Lean4

theorem map_gcd [CommGroupWithZero R] {f : ArithmeticFunction R} (hf : f.IsMultiplicative) {x y : ℕ}
    (hf_lcm : f (x.lcm y) ≠ 0) : f (x.gcd y) = f x * f y / f (x.lcm y) := by
  rw [← hf.lcm_apply_mul_gcd_apply, mul_div_cancel_left₀ _ hf_lcm]

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