English
A finite sum of rationals with positive p-adic valuations is positive in valuation if the sum is nonzero: 0 < v_p(∑ F_i).
Русский
Конечная сумма рациональных чисел с положительной p-адикальной величиной положительна по значению, если сумма не равна нулю.
LaTeX
$$$ (\\forall i, 0 \\le i < n) \\Rightarrow v_p(F_i) > 0 \\Rightarrow \\left( \\sum_{i=0}^{n-1} F_i \\neq 0 \\Rightarrow v_p\\left(\\sum_{i=0}^{n-1} F_i\\right) > 0 \\right) $$$
Lean4
/-- A finite sum of rationals with positive `p`-adic valuation has positive `p`-adic valuation
(if the sum is non-zero). -/
theorem sum_pos_of_pos {n : ℕ} {F : ℕ → ℚ} (hF : ∀ i, i < n → 0 < padicValRat p (F i))
(hn0 : ∑ i ∈ Finset.range n, F i ≠ 0) : 0 < padicValRat p (∑ i ∈ Finset.range n, F i) := by
induction n with
| zero => exact False.elim (hn0 rfl)
| succ d hd =>
rw [Finset.sum_range_succ] at hn0 ⊢
by_cases h : ∑ x ∈ Finset.range d, F x = 0
· rw [h, zero_add]
exact hF d (lt_add_one _)
· refine lt_of_lt_of_le ?_ (min_le_padicValRat_add hn0)
refine lt_min (hd (fun i hi => ?_) h) (hF d (lt_add_one _))
exact hF _ (lt_trans hi (lt_add_one _))
