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
andpadic_val_rat
in number_theory.padics.padic_norm, but nopadic_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