LFunctionTrivChar₁_apply_one_ne_zero

English

For all n, LFunctionTrivChar₁ n 1 ≠ 0 (auxiliary form).

Русский

Для всех n выполняется LFunctionTrivChar₁ n 1 ≠ 0 (вспомогательная форма).

LaTeX

$$$LFunctionTrivChar_1(n,1) \neq 0$$$

Lean4

theorem LFunctionTrivChar₁_apply_one_ne_zero : LFunctionTrivChar₁ n 1 ≠ 0 :=
  by
  simp only [Function.update_self]
  refine Finset.prod_ne_zero_iff.mpr fun p hp ↦ ?_
  simpa [sub_ne_zero] using (Nat.prime_of_mem_primeFactors hp).ne_one

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