map_div_of_coprime — Mathlib

English

Let f be multiplicative. If d|l and (l/d) ⟂ d and f(d) ≠ 0, then f(l/d) = f(l)/f(d).

Русский

Пусть f мультипликативна. Если d делит l и (l/d) взаимно простое с d, и f(d) ≠ 0, то f(l/d) = f(l)/f(d).

LaTeX

$$$f\left(\frac{l}{d}\right) = \frac{f(l)}{f(d)} \\text{при } d\mid l,\ (\tfrac{l}{d})\perp d,\ f(d)\neq 0$$$

Lean4

theorem map_div_of_coprime [GroupWithZero R] {f : ArithmeticFunction R} (hf : IsMultiplicative f) {l d : ℕ}
    (hdl : d ∣ l) (hl : (l / d).Coprime d) (hd : f d ≠ 0) : f (l / d) = f l / f d :=
  by
  apply (div_eq_of_eq_mul hd ..).symm
  rw [← hf.right hl, Nat.div_mul_cancel hdl]

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