@[reducible, inline]

abbrev FieldAbsoluteValue (k : Type u_1) [Field k] : Type u_1

def AbsoluteValue.IsArchimedean {k : Type u_1} [Field k] (v : AbsoluteValue k ℝ) : Prop

def AbsoluteValue.IsEquivalent {k : Type u_1} [Field k] (v w : AbsoluteValue k ℝ) : Prop

@[reducible, inline]

abbrev padicValuation (p : ℕ) [Fact (Nat.Prime p)] : ℚ → ℤ

@[reducible, inline]

abbrev padicAbsoluteValue (p : ℕ) [Fact (Nat.Prime p)] : ℚ → ℚ

@[reducible, inline]

abbrev padicAbsoluteValueReal (p : ℕ) [Fact (Nat.Prime p)] : AbsoluteValue ℚ ℝ

def absAbsoluteValue : AbsoluteValue ℚ ℝ

theorem ostrowski_theorem (v : AbsoluteValue ℚ ℝ) (hv : v.IsNontrivial) : v.IsEquiv absAbsoluteValue ∨ ∃ (p : ℕ) (x : Fact (Nat.Prime p)), v.IsEquiv (padicAbsoluteValueReal p)

theorem padicNorm_eq_one_of_not_dvd (x : ℚ) (p : ℕ) [hp : Fact (Nat.Prime p)] (hnum : ¬p ∣ x.num.natAbs) (hden : ¬p ∣ x.den) : padicNorm p x = 1

theorem finite_nat_primes_dvd (N : ℕ) (hN : N ≠ 0) : {p : Nat.Primes | ↑p ∣ N}.Finite

theorem PF_finsupp (x : ℚ) (hx : x ≠ 0) : (Function.mulSupport fun (p : Nat.Primes) => ↑(padicNorm (↑p) x)).Finite

theorem PF_prime (q : ℕ) (hq : Nat.Prime q) : |↑↑q| * ∏ᶠ (p : Nat.Primes), ↑(padicNorm ↑p ↑q) = 1

theorem PF_mul (a b : ℚ) (hfa : (Function.mulSupport fun (p : Nat.Primes) => ↑(padicNorm (↑p) a)).Finite) (hfb : (Function.mulSupport fun (p : Nat.Primes) => ↑(padicNorm (↑p) b)).Finite) (ha1 : |↑a| * ∏ᶠ (p : Nat.Primes), ↑(padicNorm (↑p) a) = 1) (hb1 : |↑b| * ∏ᶠ (p : Nat.Primes), ↑(padicNorm (↑p) b) = 1) : |↑(a * b)| * ∏ᶠ (p : Nat.Primes), ↑(padicNorm (↑p) (a * b)) = 1

theorem PF_nat_pos (n : ℕ) (hn : 0 < n) : |↑↑n| * ∏ᶠ (p : Nat.Primes), ↑(padicNorm ↑p ↑n) = 1

theorem PF_int (z : ℤ) (hz : z ≠ 0) : |↑↑z| * ∏ᶠ (p : Nat.Primes), ↑(padicNorm ↑p ↑z) = 1

theorem product_formula (x : ℚ) (hx : x ≠ 0) : |↑x| * ∏ᶠ (p : Nat.Primes), ↑(padicNorm (↑p) x) = 1

theorem AbsoluteValue.pow_le_mul_max_pow {k : Type u_1} [Field k] (v : AbsoluteValue k ℝ) (hv : ∀ (n : ℕ), v ↑n ≤ 1) (x y : k) (n : ℕ) : v (x + y) ^ n ≤ (↑n + 1) * max (v x) (v y) ^ n

theorem AbsoluteValue.isNonarchimedean_iff_natCast_le_one {k : Type u_1} [Field k] (v : AbsoluteValue k ℝ) : IsNonarchimedean ⇑v ↔ ∀ (n : ℕ), 0 < n → v (n • 1) ≤ 1

theorem lemma_1_4_forward {k : Type u_1} [Field k] (v : AbsoluteValue k ℝ) (hv : IsNonarchimedean ⇑v) (n : ℕ) : v ↑n ≤ 1

theorem lemma_1_4 {k : Type u_1} [Field k] (v : AbsoluteValue k ℝ) : IsNonarchimedean ⇑v ↔ ∀ (n : ℕ), v ↑n ≤ 1

theorem corollary_1_5_part1 {k : Type u_1} [Field k] {p : ℕ} [CharP k p] (hp : p ≠ 0) (v : AbsoluteValue k ℝ) : IsNonarchimedean ⇑v

theorem corollary_1_5_part2 {k : Type u_1} [Field k] [Fintype k] (v : AbsoluteValue k ℝ) (x : k) : x ≠ 0 → v x = 1

theorem absValue_charP_isNonarchimedean_and_finite_trivial {k : Type u_1} [Field k] (v : AbsoluteValue k ℝ) {p : ℕ} [CharP k p] (hp : p ≠ 0) : IsNonarchimedean ⇑v ∧ ∀ [Fintype k] (x : k), x ≠ 0 → v x = 1