p-adic numbers and local fields

p-adic integers and expansions, valuations of integer sequences, Hensel lifting, Strassmann's theorem, Hilbert symbols, p-adic gamma, local fields.

TheoremCassels' embedding theorem#✓fully proved

Let \(K\) be a field of characteristic zero and \(S\) a finite subset of \(K\). Then there are a prime \(p \ge 3\) and an injective ring homomorphism from the subring of \(K\) generated by \(S\) into the ring \(\mathbb{Z}_p\) of \(p\)-adic integers.

public theorem exists_injective_ringHom_closure_padicInt {K : Type*} [Field K] [CharZero K]
    (S : Finset K) :
    ∃ (p : ℕ) (hp : p.Prime),
      letI : Fact p.Prime := ⟨hp⟩
      3 ≤ p ∧ ∃ phi : Subring.closure (↑S : Set K) →+* ℤ_[p],
        Function.Injective phi

Sources

J. W. S. Cassels, "An embedding theorem for fields", Bull. Austral. Math. Soc. 14 (1976), 193–198.

Used by 1

Used bySkolem–Mahler–Lech theorem

Theoremp-adic integrality is equivalent to norm at most one#✓fully proved

An element of the algebraic closure of ℚ_[p] is integral over ℤ_[p] if and only if its norm is at most one.

theorem isIntegral_padicInt_iff_norm_le_one (p : ℕ) [Fact p.Prime] (x : PadicAlgCl p) :
    IsIntegral ℤ_[p] x ↔ ‖x‖ ≤ 1

TheoremStrassmann's theorem#✓fully proved

Let \(p\) be a prime and let \((b_m)_{m \ge 0}\) be a sequence in \(\mathbb{Q}_p\), not identically zero, with \(b_m \to 0\). Then the power series \(\sum_{m \ge 0} b_m y^m\) has only finitely many zeros \(y \in \mathbb{Q}_p\) with \(|y|_p \le 1\).

public theorem strassmann (p : ℕ) [Fact p.Prime] (b : ℕ → ℚ_[p])
    (hb : Filter.Tendsto b Filter.cofinite (nhds 0)) (hne : b ≠ 0) :
    {y : ℚ_[p] | ‖y‖ ≤ 1 ∧ ∑' m, b m * y ^ m = 0}.Finite

Sources

R. Strassmann, J. Reine Angew. Math. 159 (1928).

Used by 1

Used bySkolem–Mahler–Lech theorem

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.