@[reducible, inline]

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

An absolute value on a field $k$ is an AbsoluteValue with codomain $\mathbb{R}$.

theorem AbsoluteValueOnField.nonneg {k : Type u_1} [Field k] (v : AbsoluteValueOnField k) (x : k) : 0 ≤ v x

The value $v(x)$ of an absolute value is always non-negative: $0 \le v(x)$.

theorem AbsoluteValueOnField.eq_zero_iff {k : Type u_1} [Field k] (v : AbsoluteValueOnField k) (x : k) : v x = 0 ↔ x = 0

Non-degeneracy of an absolute value: $v(x) = 0 \iff x = 0$.

theorem AbsoluteValueOnField.thm_5_3c_forward {k : Type u_1} [Field k] (v : AbsoluteValueOnField k) (hna : IsNonarchimedean ⇑v) (n : ℕ) : v ↑n ≤ 1

Theorem 5.3(c), forward direction: if $v$ is nonarchimedean then $v(n) \le 1$ for every $n \in \mathbb{N}$.

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

Binomial-type bound: assuming $v(n) \le 1$ for every $n$, one has $v(x+y)^n \le (n+1) \max(v(x), v(y))^n$ for all $n$.

theorem AbsoluteValueOnField.le_of_pow_le_mul_pow (r M : ℝ) (hM : 0 ≤ M) (h : ∀ (n : ℕ), r ^ n ≤ (↑n + 1) * M ^ n) : r ≤ M

If $r^n \le (n+1) M^n$ holds for every natural number $n$ (with $M \ge 0$), then $r \le M$.

theorem AbsoluteValueOnField.thm_5_3c_backward {k : Type u_1} [Field k] (v : AbsoluteValueOnField k) (hv : ∀ (n : ℕ), v ↑n ≤ 1) : IsNonarchimedean ⇑v

Theorem 5.3(c), backward direction: if $v(n) \le 1$ for every $n \in \mathbb{N}$, then $v$ is nonarchimedean.

theorem AbsoluteValueOnField.thm_5_3c {k : Type u_1} [Field k] (v : AbsoluteValueOnField k) : IsNonarchimedean ⇑v ↔ ∀ (n : ℕ), v ↑n ≤ 1

Theorem 5.3(c): an absolute value $v$ is nonarchimedean iff $v(n) \le 1$ for all natural numbers $n$.

theorem AbsoluteValueOnField.eq_one_of_pow_eq_one_of_pos {a : ℝ} (ha : 0 < a) {n : ℕ} (hn : n ≠ 0) (h : a ^ n = 1) : a = 1

If $a > 0$, $n \ne 0$, and $a^n = 1$, then $a = 1$.

theorem AbsoluteValueOnField.natCast_pow_charP {k : Type u_1} [Field k] (p : ℕ) [CharP k p] [Fact (Nat.Prime p)] (n : ℕ) : ↑n ^ p = ↑n

In a field $k$ of characteristic $p$, the Frobenius identity reads $(n : k)^p = n$ for every natural number $n$.

theorem AbsoluteValueOnField.natCast_pow_char_sub_one_eq_one {k : Type u_1} [Field k] (p : ℕ) [CharP k p] [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : ↑n ≠ 0) : ↑n ^ (p - 1) = 1

Fermat's little theorem in $k$: if $\mathrm{char}(k) = p$ is prime and $(n : k) \ne 0$, then $(n : k)^{p-1} = 1$.

theorem AbsoluteValueOnField.cor_5_4_nonarchimedean {k : Type u_1} [Field k] (v : AbsoluteValueOnField k) (p : ℕ) [CharP k p] [hp : Fact (Nat.Prime p)] : IsNonarchimedean ⇑v

Corollary 5.4: any absolute value on a field of prime characteristic is nonarchimedean.

def AbsoluteValueOnField.AreEquivalent {k : Type u_1} [Field k] (v₁ v₂ : AbsoluteValue k ℝ) : Prop

Definition 5.5: two absolute values $v_1, v_2$ on $k$ are equivalent if there exists $\alpha > 0$ such that $v_2(x) = v_1(x)^\alpha$ for every $x \in k$.

theorem AbsoluteValueOnField.areEquivalent_iff_isEquiv {k : Type u_1} [Field k] (v₁ v₂ : AbsoluteValue k ℝ) : AreEquivalent v₁ v₂ ↔ v₁.IsEquiv v₂

The custom AreEquivalent relation coincides with the Mathlib AbsoluteValue.IsEquiv relation.

theorem AbsoluteValueOnField.ostrowski (v : AbsoluteValue ℚ ℝ) (hv : v.IsNontrivial) : AreEquivalent v Rat.AbsoluteValue.real ∨ ∃ (p : ℕ) (x : Fact (Nat.Prime p)), AreEquivalent v (Rat.AbsoluteValue.padic p)

Theorem 5.6 (Ostrowski's theorem for $\mathbb{Q}$): every nontrivial absolute value on $\mathbb{Q}$ is equivalent either to the real absolute value $|\cdot|_\infty$ or to a $p$-adic absolute value $|\cdot|_p$ for some prime $p$.