isMultiplicative_one — Mathlib

English

The constant-1 function is multiplicative: for coprime m,n, 1(mn) = 1(m) 1(n).

Русский

Постоянно-единичная функция мультипликативна: для взаимно простых m,n выполняется 1(mn) = 1(m) 1(n).

LaTeX

$$$ IsMultiplicative(1) $$$

Lean4

@[arith_mult]
theorem isMultiplicative_one [MonoidWithZero R] : IsMultiplicative (1 : ArithmeticFunction R) :=
  IsMultiplicative.iff_ne_zero.2
    ⟨by simp, by
      intro m n hm _hn hmn
      rcases eq_or_ne m 1 with (rfl | hm')
      · simp
      rw [one_apply_ne, one_apply_ne hm', zero_mul]
      rw [Ne, mul_eq_one, not_and_or]
      exact Or.inl hm'⟩

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