Theorems · Theorem · number theory

padicValRat.lt_sum_of_lt

∀ {p j : ℕ} [hp : Fact (Nat.Prime p)] {F : ℕ → ℚ} {S : Finset ℕ},
  S.Nonempty →
    (∀ i ∈ S, padicValRat p (F j) < padicValRat p (F i)) →
      (∀ (i : ℕ), 0 < F i) → padicValRat p (F j) < padicValRat p (∑ i ∈ S, F i)

If the p-adic valuation of a finite set of positive rationals is greater than a given rational number, then the p-adic valuation of their sum is also greater than the same rational number.

Defined in

Mathlib.NumberTheory.Padics.PadicVal.Basic

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact