Theorems · Definition · number theory

PadicInt.mahlerSeries

{p : ℕ} →
  [hp : Fact (Nat.Prime p)] →
    {E : Type u_1} →
      [inst : NormedAddCommGroup E] → [inst_1 : Module ℤ_[p] E] → [IsBoundedSMul ℤ_[p] E] → (ℕ → E) → C(ℤ_[p], E)

A series of the form considered in Mahler's theorem.

Defined in

Mathlib.NumberTheory.Padics.MahlerBasis

Cited by

9 results in Mathlib

Foundations

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

Assumes

FactNormedAddCommGroupModuleIsBoundedSMul