feat(number_theory/padics/padic_norm): add int_eq_one_iff (#16074)

Add the proof that the p-adic norm of an integer is 1 iff the integer is not a multiple of p and related API for `padic_norm`.

src/number_theory/padics/padic_norm.lean

@@ -46,7 +46,6 @@ if q = 0 then 0 else (↑p : ℚ) ^ (-(padic_val_rat p q))
 
 namespace padic_norm
 
-section padic_norm
 open padic_val_rat
 variables (p : ℕ)
 
@@ -286,5 +285,93 @@ begin
     { exact_mod_cast hp.1.one_lt } }
 end
 
-end padic_norm
+/-- The `p`-adic norm of an integer `m` is one iff `p` doesn't divide `m`. -/
+lemma int_eq_one_iff (m : ℤ) : padic_norm p m = 1 ↔ ¬ (p : ℤ) ∣ m :=
+begin
+  nth_rewrite 1 ← pow_one p,
+  simp only [dvd_iff_norm_le, int.cast_coe_nat, nat.cast_one, zpow_neg, zpow_one, not_le],
+  split,
+  { intro h,
+    rw [h, inv_lt_one_iff_of_pos];
+    norm_cast,
+    { exact nat.prime.one_lt (fact.out _), },
+    { exact nat.prime.pos (fact.out _), }, },
+  { simp only [padic_norm],
+    split_ifs,
+    { rw [inv_lt_zero, ← nat.cast_zero, nat.cast_lt],
+      intro h, exact (nat.not_lt_zero p h).elim, },
+    { have : 1 < (p : ℚ) := by norm_cast; exact (nat.prime.one_lt (fact.out _ : nat.prime p)),
+      rw [← zpow_neg_one, zpow_lt_iff_lt this],
+      have : 0 ≤ padic_val_rat p m, simp only [of_int, nat.cast_nonneg],
+      intro h,
+      rw [← zpow_zero (p : ℚ), zpow_inj];
+      linarith, } },
+end
+
+lemma int_lt_one_iff (m : ℤ) : padic_norm p m < 1 ↔ (p : ℤ) ∣ m :=
+begin
+  rw [← not_iff_not, ← int_eq_one_iff, eq_iff_le_not_lt],
+  simp only [padic_norm.of_int, true_and],
+end
+
+lemma of_nat (m : ℕ) : padic_norm p m ≤ 1 :=
+padic_norm.of_int p (m : ℤ)
+
+/-- The `p`-adic norm of a natural `m` is one iff `p` doesn't divide `m`. -/
+lemma nat_eq_one_iff (m : ℕ) : padic_norm p m = 1 ↔ ¬ p ∣ m :=
+by simp only [←int.coe_nat_dvd, ←int_eq_one_iff, int.cast_coe_nat]
+
+lemma nat_lt_one_iff (m : ℕ) : padic_norm p m < 1 ↔ p ∣ m :=
+by simp only [←int.coe_nat_dvd, ←int_lt_one_iff, int.cast_coe_nat]
+
+open_locale big_operators
+
+lemma sum_lt {α : Type*} {F : α → ℚ} {t : ℚ} {s : finset α} :
+  s.nonempty → (∀ i ∈ s, padic_norm p (F i) < t) →
+  padic_norm p (∑ i in s, F i) < t :=
+begin
+  classical,
+  refine s.induction_on (by { rintro ⟨-, ⟨⟩⟩, }) _,
+  rintro a S haS IH - ht,
+  by_cases hs : S.nonempty,
+  { rw finset.sum_insert haS,
+    exact lt_of_le_of_lt (padic_norm.nonarchimedean p) (max_lt
+      (ht a (finset.mem_insert_self a S))
+      (IH hs (λ b hb, ht b (finset.mem_insert_of_mem hb)))), },
+  { simp * at *, },
+end
+
+lemma sum_le {α : Type*} {F : α → ℚ} {t : ℚ} {s : finset α} :
+  s.nonempty → (∀ i ∈ s, padic_norm p (F i) ≤ t) →
+  padic_norm p (∑ i in s, F i) ≤ t :=
+begin
+  classical,
+  refine s.induction_on (by { rintro ⟨-, ⟨⟩⟩, }) _,
+  rintro a S haS IH - ht,
+  by_cases hs : S.nonempty,
+  { rw finset.sum_insert haS,
+    exact (padic_norm.nonarchimedean p).trans (max_le
+      (ht a (finset.mem_insert_self a S))
+      (IH hs (λ b hb, ht b (finset.mem_insert_of_mem hb)))), },
+  { simp * at *, },
+end
+
+lemma sum_lt' {α : Type*} {F : α → ℚ} {t : ℚ} {s : finset α}
+  (hF : ∀ i ∈ s, padic_norm p (F i) < t) (ht : 0 < t) :
+  padic_norm p (∑ i in s, F i) < t :=
+begin
+  obtain rfl | hs := finset.eq_empty_or_nonempty s,
+  { simp [ht], },
+  { exact sum_lt hs hF, },
+end
+
+lemma sum_le' {α : Type*} {F : α → ℚ} {t : ℚ} {s : finset α}
+  (hF : ∀ i ∈ s, padic_norm p (F i) ≤ t) (ht : 0 ≤ t) :
+  padic_norm p (∑ i in s, F i) ≤ t :=
+begin
+  obtain rfl | hs := finset.eq_empty_or_nonempty s,
+  { simp [ht], },
+  { exact sum_le hs hF, },
+end
+
 end padic_norm