Theorems · Theorem · number theory

PadicInt.appr.eq_def

∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) (x_1 : ℕ),
  x.appr x_1 =
    match x, x_1 with
    | _x, 0 => 0
    | x, n.succ =>
      have y := x - ↑(x.appr n);
      if hy : y = 0 then x.appr n
      else
        have u := ↑(PadicInt.unitCoeff hy);
        x.appr n + p ^ n * (PadicInt.toZMod (u * ↑p ^ (↑y.valuation - ↑n).natAbs)).val

Defined in

Mathlib.NumberTheory.Padics.RingHoms

Cited by

0 results in Mathlib

Foundations

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

Assumes

Fact