feat(Data/Nat/DivSequence): add divisibility sequences and strong divisibility sequences (#41204)

This PR moves divisibility sequences from `NumberTheory/EllipticDivisibilitySequence.lean` to a new file `Data/Nat/DivSequence.lean` and adds strong divisibility sequences.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib.lean

@@ -4184,6 +4184,7 @@ public import Mathlib.Data.Nat.Digits.Defs
 public import Mathlib.Data.Nat.Digits.Div
 public import Mathlib.Data.Nat.Digits.Lemmas
 public import Mathlib.Data.Nat.Dist
+public import Mathlib.Data.Nat.DvdSequence
 public import Mathlib.Data.Nat.EvenOddRec
 public import Mathlib.Data.Nat.Factorial.Basic
 public import Mathlib.Data.Nat.Factorial.BigOperators

Mathlib/Data/Nat/DvdSequence.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Thomas Browning. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning
+-/
+module
+
+public import Mathlib.Algebra.Divisibility.Basic
+public import Mathlib.Algebra.Group.Action.Pi
+
+/-!
+# Divisibility sequences
+
+A sequence `f : ℕ → ℕ` is a *divisibility sequence* if it satisfies `f a ∣ f b` whenever `a ∣ b`.
+
+A sequence `f : ℕ → ℕ` is a *strong divisibility sequence* if `gcd (f a) (f b) = f (gcd a b)`.
+
+This file defines divisibility sequences and strong divisibility sequences, and provides some basic
+API for these definitions.
+
+## Main definitions
+
+* `IsDvdSeq`: A function `f` is a divisibility sequence if `a ∣ b` implies `f a ∣ f b`.
+* `Nat.IsStrongDvdSeq`: A function `f : ℕ → ℕ` is a strong divisibility sequence if `f` satisfies
+  `gcd (f a) (f b) = f (gcd a b)`.
+-/
+
+@[expose] public section
+
+variable {α β γ : Type*}
+
+-- this lemma regarding interaction between `smul` and `dvd` does not have a good home in mathlib
+lemma smul_dvd_smul [Monoid α] [Monoid β] [SMul α β] [IsScalarTower α β β]
+    [IsScalarTower α α β] [SMulCommClass α β β] {a b : α} {c d : β}
+    (hab : a ∣ b) (hcd : c ∣ d) : (a • c) ∣ (b • d) := by
+  obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := hab, hcd
+  exact ⟨x • y, mul_smul_mul_comm a x c y⟩
+
+/-- A function `f : α → β` is a divisibility sequence if `a ∣ b` implies `f a ∣ f b`. -/
+def IsDvdSequence [Dvd α] [Dvd β] (f : α → β) : Prop :=
+  ∀ a b, a ∣ b → f a ∣ f b
+
+namespace IsDvdSequence
+
+variable (α) in
+protected theorem id [Dvd α] : IsDvdSequence (id : α → α) :=
+  fun _ _ ↦ id
+
+variable (α) in
+protected theorem const [Dvd α] [Monoid β] (b : β) : IsDvdSequence (fun _ : α ↦ b) := by
+  simp [IsDvdSequence]
+
+protected theorem smul' [Dvd α] [Monoid β] [Monoid γ] {f : α → β} {g : α → γ} [SMul β γ]
+    [IsScalarTower β γ γ] [IsScalarTower β β γ] [SMulCommClass β γ γ]
+    (hf : IsDvdSequence f) (hg : IsDvdSequence g) : IsDvdSequence (f • g) :=
+  fun a b hab ↦ smul_dvd_smul (hf a b hab) (hg a b hab)
+
+protected theorem mul [Dvd α] [CommMonoid β] {f g : α → β}
+    (hf : IsDvdSequence f) (hg : IsDvdSequence g) : IsDvdSequence (f * g) :=
+  .smul' hf hg
+
+protected theorem smul [Dvd α] [Monoid β] [Monoid γ] {f : α → γ} [SMul β γ]
+    [IsScalarTower β γ γ] [IsScalarTower β β γ] [SMulCommClass β γ γ]
+    (b : β) (hg : IsDvdSequence f) : IsDvdSequence (b • f) :=
+  .smul' (.const α b) hg
+
+end IsDvdSequence
+
+namespace Nat
+
+/-- A function `f : ℕ → ℕ` is a strong divisibility sequence if `gcd (f a) (f b) = f (gcd a b)`. -/
+def IsStrongDvdSequence (f : ℕ → ℕ) : Prop :=
+  ∀ a b, (f a).gcd (f b) = f (a.gcd b)
+
+namespace IsStrongDvdSequence
+
+theorem isDvdSequence {f : ℕ → ℕ} (hf : IsStrongDvdSequence f) : IsDvdSequence f := by
+  intro a b hab
+  simpa [gcd_eq_left hab, gcd_eq_left_iff_dvd] using hf a b
+
+protected theorem id : IsStrongDvdSequence (id : ℕ → ℕ) :=
+  fun _ _ ↦ rfl
+
+protected theorem const (n : ℕ) : IsStrongDvdSequence (fun _ ↦ n) := by
+  simp [IsStrongDvdSequence]
+
+end IsStrongDvdSequence
+
+end Nat

Mathlib/Data/Nat/Fib/Basic.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Data.Finset.NatAntidiagonal
 public import Mathlib.Data.Nat.GCD.Basic
 public import Mathlib.Data.Nat.BinaryRec
+public import Mathlib.Data.Nat.DvdSequence
 public import Mathlib.Logic.Function.Iterate
 public import Mathlib.Tactic.Ring
 public import Mathlib.Tactic.Zify
@@ -243,8 +244,13 @@ theorem fib_gcd (m n : ℕ) : fib (gcd m n) = gcd (fib m) (fib n) := by
     conv_rhs => rw [← mod_add_div' n m]
     rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
 
-theorem fib_dvd (m n : ℕ) (h : m ∣ n) : fib m ∣ fib n := by
-  rwa [← gcd_eq_left_iff_dvd, ← fib_gcd, gcd_eq_left_iff_dvd.mpr]
+theorem isStrongDvdSequence_fib : IsStrongDvdSequence fib :=
+  fun m n ↦ (fib_gcd m n).symm
+
+theorem isDvdSequence_fib : IsDvdSequence fib :=
+  isStrongDvdSequence_fib.isDvdSequence
+
+alias fib_dvd := isDvdSequence_fib
 
 theorem fib_succ_eq_sum_choose :
     ∀ n : ℕ, fib (n + 1) = ∑ p ∈ Finset.antidiagonal n, choose p.1 p.2 :=

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

@@ -5,6 +5,7 @@ Authors: David Kurniadi Angdinata
 -/
 module
 
+public import Mathlib.Data.Nat.DvdSequence
 public import Mathlib.Data.Nat.EvenOddRec
 public import Mathlib.Tactic.Linarith
 public import Mathlib.Tactic.LinearCombination
@@ -30,7 +31,6 @@ Some examples of EDSs include
 ## Main definitions
 
 * `IsEllSequence`: a sequence indexed by integers is an elliptic sequence.
-* `IsDivSequence`: a sequence indexed by integers is a divisibility sequence.
 * `IsEllDivSequence`: a sequence indexed by integers is an EDS.
 * `preNormEDS'`: the auxiliary sequence for a normalised EDS indexed by `ℕ`.
 * `preNormEDS`: the auxiliary sequence for a normalised EDS indexed by `ℤ`.
@@ -83,32 +83,28 @@ def IsEllSequence : Prop :=
   ∀ m n r : ℤ, W (m + n) * W (m - n) * W r ^ 2 =
     W (m + r) * W (m - r) * W n ^ 2 - W (n + r) * W (n - r) * W m ^ 2
 
-/-- The proposition that a sequence indexed by integers is a divisibility sequence. -/
-def IsDivSequence : Prop :=
-  ∀ m n : ℕ, m ∣ n → W m ∣ W n
+@[deprecated (since := "2026-06-30")] alias IsDivSequence := IsDvdSequence
 
 /-- The proposition that a sequence indexed by integers is an EDS. -/
 def IsEllDivSequence : Prop :=
-  IsEllSequence W ∧ IsDivSequence W
+  IsEllSequence W ∧ IsDvdSequence W
 
 lemma isEllSequence_id : IsEllSequence id :=
   fun _ _ _ => by simp_rw [id_eq]; ring1
 
-lemma isDivSequence_id : IsDivSequence id :=
-  fun _ _ => Int.ofNat_dvd.mpr
+@[deprecated (since := "2026-06-30")] alias isDivSequence_id := IsDvdSequence.id
 
 /-- The identity sequence is an EDS. -/
 theorem isEllDivSequence_id : IsEllDivSequence id :=
-  ⟨isEllSequence_id, isDivSequence_id⟩
+  ⟨isEllSequence_id, .id ℤ⟩
 
 variable {W}
 
 lemma IsEllSequence.smul (h : IsEllSequence W) (x : R) : IsEllSequence (x • W) :=
   fun m n r => by
     linear_combination (norm := (simp_rw [Pi.smul_apply, smul_eq_mul]; ring1)) x ^ 4 * h m n r
 
-lemma IsDivSequence.smul (h : IsDivSequence W) (x : R) : IsDivSequence (x • W) :=
-  fun m n r => mul_dvd_mul_left x <| h m n r
+@[deprecated (since := "2026-06-30")] alias IsDivSequence.smul := IsDvdSequence.smul
 
 lemma IsEllDivSequence.smul (h : IsEllDivSequence W) (x : R) : IsEllDivSequence (x • W) :=
   ⟨h.left.smul x, h.right.smul x⟩