Zulip Chat Archive

Stream: Is there code for X?

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


Michael Stoll (Mar 22 2022 at 11:11):

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 (Mar 22 2022 at 11:12):

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 (Mar 22 2022 at 11:13):

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 (Mar 22 2022 at 11:15):

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

Ruben Van de Velde (Mar 22 2022 at 11:19):

docs#padic_norm_e.norm_int_lt_one_iff_dvd seems interesting

Ruben Van de Velde (Mar 22 2022 at 11:25):

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 (Mar 22 2022 at 11:29):

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 (Mar 22 2022 at 11:30):

(Mine has only five lines...)

Michael Stoll (Mar 22 2022 at 11:31):

But I find the change and by norm_cast stuff annoying.

Bolton Bailey (Mar 22 2022 at 14:06):

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 (Mar 22 2022 at 18:32):

Does this also add the necessary API lemmas?

Bolton Bailey (Mar 23 2022 at 16:53):

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 (Mar 23 2022 at 20:13):

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

Michael Stoll (Mar 23 2022 at 20:48):

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

Last updated: Dec 20 2023 at 11:08 UTC