eq_zero_of_squarefree_of_dvd_eq_zero

English

If f is multiplicative and m|n with n squarefree and f(m)=0, then f(n)=0.

Русский

Если f мультипликативна и m делит n, n квадратно-безповторное и f(m)=0, то f(n)=0.

LaTeX

$$$\text{If } n\text{ squarefree and } m|n \text{ with } f(m)=0, \ \ f(n)=0$$$

Lean4

theorem eq_zero_of_squarefree_of_dvd_eq_zero [MonoidWithZero R] {f : ArithmeticFunction R} (hf : IsMultiplicative f)
    {m n : ℕ} (hn : Squarefree n) (hmn : m ∣ n) (h_zero : f m = 0) : f n = 0 :=
  by
  rcases hmn with ⟨k, rfl⟩
  simp only [zero_mul, hf.map_mul_of_coprime (coprime_of_squarefree_mul hn), h_zero]

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