feat: add zeta_sub_one_dvd_intCast_iff and related declarations (leanprover-community#40232)

Author: riccardobrasca

Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

@@ -72,6 +72,14 @@ theorem associated_norm_zeta_sub_one : Associated (Algebra.norm ℤ (hζ.toInteg
       rw [hζ.norm_toInteger_sub_one_of_eq_two_pow, h, Int.ofNat_two]
   · rw [hζ.norm_toInteger_sub_one_of_prime_ne_two h]
 
+/-- An integer `n` is divisible by `ζ - 1` in `𝓞 K` if and only if it is divisible by `p`,
+where `ζ` is a primitive `p ^ (k + 1)`-th root of unity. -/
+theorem zeta_sub_one_dvd_intCast_iff {n : ℤ} :
+    hζ.toInteger - 1 ∣ (n : 𝓞 K) ↔ (p : ℤ) ∣ n := by
+  have h := associated_norm_zeta_sub_one p k hζ
+  rw [← Ideal.norm_dvd_iff (h.symm.prime (Nat.prime_iff_prime_int.mp hp.out))]
+  exact h.dvd_iff_dvd_left
+
 theorem absNorm_span_zeta_sub_one : absNorm (span {hζ.toInteger - 1}) = p := by
   simpa using congr_arg absNorm <|
     span_singleton_eq_span_singleton.mpr <| associated_norm_zeta_sub_one p k hζ
@@ -231,6 +239,13 @@ theorem ramificationIdx_span_zeta_sub_one' :
   rw [← pow_one p] at hK hζ
   rw [ramificationIdx_span_zeta_sub_one p 0 hζ, pow_zero, one_mul]
 
+/-- An integer `n` is divisible by `ζ - 1` in `𝓞 K` if and only if it is divisible by `p`,
+where `ζ` is a primitive `p`-th root of unity. -/
+theorem zeta_sub_one_dvd_intCast_iff' {n : ℤ} :
+    hζ.toInteger - 1 ∣ (n : 𝓞 K) ↔ (p : ℤ) ∣ n := by
+  rw [← pow_one p] at hK hζ
+  exact zeta_sub_one_dvd_intCast_iff p 0 hζ
+
 variable (K)
 
 include hK in

Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean

@@ -150,6 +150,16 @@ lemma nthRootsFinset_pairwise_associated_sub_one_sub_of_prime (hζ : IsPrimitive
 alias ntRootsFinset_pairwise_associated_sub_one_sub_of_prime :=
   nthRootsFinset_pairwise_associated_sub_one_sub_of_prime
 
+/-- If `p` is prime and `ζ` is a `p`-th primitive root of unity, then `ζ - 1` divides `η₁ - η₂`
+for all `p`-th roots of unity `η₁` and `η₂`. -/
+lemma sub_one_dvd_sub (hζ : IsPrimitiveRoot ζ p) (hp : p.Prime)
+    {η₁ : A} (hη₁ : η₁ ∈ nthRootsFinset p (1 : A))
+    {η₂ : A} (hη₂ : η₂ ∈ nthRootsFinset p (1 : A)) :
+    ζ - 1 ∣ η₁ - η₂ := by
+  rcases eq_or_ne η₁ η₂ with rfl | h
+  · simp
+  · exact (hζ.nthRootsFinset_pairwise_associated_sub_one_sub_of_prime hp hη₁ hη₂ h).dvd
+
 /-- Given an `n`-th primitive root of unity `ζ`, where `1 < n`, we have that `ζ - 1` divides `n`.
   In particular, if `ζ` is a `p`-th primitive root of unity with `p` prime, then `ζ - 1` divides
   `p`. -/