p-adic norm of (a : int) = 1 from p not dividing a?

Stream: Is there code for X?

[Michael Stoll]

Is there a simple proof of

lemma padic_norm.padic_norm_eq_one_of_not_dvd (p : ℕ) [fact p.prime] (a : ℤ) (ha : ¬ ↑p ∣ a) : ∥(a : ℤ_[p])∥ = 1

from what is in mathlib?

[Michael Stoll]

I see a lot of padic_val_nat and padic_val_rat in number_theory.padics.padic_norm, but no padic_val_int, which I find surprising.

[Michael Stoll]

OK, the nat version is there: docs#padic_val_nat_of_not_dvd . So I'll guess I have to use that, but having to convert integers to naturals is a pain...

[Michael Stoll]

Plus, I'm stumbling over the differences between norm, padic_norm_e and padic_norm.

[Ruben Van de Velde]

docs#padic_norm_e.norm_int_lt_one_iff_dvd seems interesting

[Ruben Van de Velde]

lemma padic_norm.padic_norm_eq_one_of_not_dvd (p : ℕ) [fact p.prime] (a : ℤ) (ha : ¬ ↑p ∣ a) :
  ∥(a : ℤ_[p])∥ = 1 := begin
  rw padic_int.norm_def,
  apply eq_of_le_of_not_lt,
  { have := @padic_norm_e.norm_int_le_one p _ a,
    convert this using 2,
    simp, },
  { norm_cast, rwa padic_norm_e.norm_int_lt_one_iff_dvd, }
end

[Michael Stoll]

lemma padic_norm.padic_norm_eq_one_of_not_dvd (p : ℕ) [hp : fact p.prime] (a : ℤ) (ha : ¬ ↑p ∣ a) :
  ∥(a : ℤ_[p])∥ = 1 :=
begin
  have hle := @padic_norm_e.norm_int_le_one p hp a,
  have hnlt := mt (@padic_norm_e.norm_int_lt_one_iff_dvd p hp a).mp ha,
  change ∥((a : ℤ_[p]) : ℚ_[p])∥ = 1,
  rw (by norm_cast : ((a : ℤ_[p]) : ℚ_[p]) = (a : ℚ_[p])),
  linarith,
end

[Michael Stoll]

(Mine has only five lines...)

[Michael Stoll]

But I find the change and by norm_cast stuff annoying.

[Bolton Bailey]

Michael Stoll said:

I see a lot of padic_val_nat and padic_val_rat in number_theory.padics.padic_norm, but no padic_val_int, which I find surprising.

#12454 adds padic_val_int

[Michael Stoll]

Does this also add the necessary API lemmas?

[Bolton Bailey]

This PR refactors padic_val_rat to depend on padic_val_nat instead of the other way around, and defines padic_val_int based on padic_val_nat as a part of it. There is a padic_val_int.eq_zero_of_not_dvd - feel free to review the PR if there are other things you want in terms of API.

[Michael Stoll]

@Bolton Bailey I have added a few comments to #12454.

[Michael Stoll]

Is there a better way of doing the following?

lemma to_zmod_pow_eq_one (p n : ℕ) [fact p.prime] (u : ℤ_[p]) (hu : padic_int.to_zmod_pow n u = 1) :
  ∃ a : ℤ_[p], u = p^n*a + 1 :=
begin
  have h₁ : padic_int.to_zmod_pow n (u - 1) = 0 :=
  by simp only [hu, _root_.map_sub, _root_.map_one, sub_self],
  have h₂ : (u - 1) ∈ (@padic_int.to_zmod_pow p _ n).ker :=
  by { simp only [ring_hom.ker], exact h₁, },
  rw [padic_int.ker_to_zmod_pow, ideal.mem_span_singleton'] at h₂,
  cases h₂ with a h₂,
  use a,
  rw ← add_eq_of_eq_sub h₂,
  ring,
end