map_lcm — Mathlib

English

If f is multiplicative, and f(x gcd y) ≠ 0, then f(x lcm y) = f x · f y / f(x gcd y).

Русский

Если f мультипликативна и f(x gcd y) ≠ 0, то f(x lcm y) = f x · f y / f(x gcd y).

LaTeX

$$$f(x\mathrm{lcm} y) = \dfrac{f(x)f(y)}{f(x\mathrm{gcd} y)}$$$

Lean4

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

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