English
For monoid-with-zero, f is multiplicative iff f(1)=1 and f(mn)=f(m)f(n) for all nonzero m,n with gcd(m,n)=1.
Русский
Для моноида с нулём: f мультипликативна тогда и только тогда, когда f(1)=1 и для всех ненулевых m,n с gcd(m,n)=1 выполняется f(mn)=f(m)f(n).
LaTeX
$$$\operatorname{IsMultiplicative}(f) \iff \bigl(f(1)=1 \land \forall m\neq 0,n\neq 0,\ m\perp n \Rightarrow f(mn)=f(m)f(n)\bigr)$$$
Lean4
/-- A recapitulation of the definition of multiplicative that is simpler for proofs -/
theorem iff_ne_zero [MonoidWithZero R] {f : ArithmeticFunction R} :
IsMultiplicative f ↔ f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n :=
by
refine and_congr_right' (forall₂_congr fun m n => ⟨fun h _ _ => h, fun h hmn => ?_⟩)
rcases eq_or_ne m 0 with (rfl | hm)
· simp
rcases eq_or_ne n 0 with (rfl | hn)
· simp
exact h hm hn hmn
