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).

theorem smul_dvd_smul {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [SMul α β] [IsScalarTower α β β] [IsScalarTower α α β] [SMulCommClass α β β] {a b : α} {c d : β} (hab : a ∣ b) (hcd : c ∣ d) : a • c ∣ b • d

def IsDvdSequence {α : Type u_1} {β : Type u_2} [Dvd α] [Dvd β] (f : α → β) : Prop

A function f : α → β is a divisibility sequence if a ∣ b implies f a ∣ f b.

Equations

• IsDvdSequence f = ∀ (a b : α), a ∣ b → f a ∣ f b

@[deprecated IsDvdSequence (since := "2026-06-30")]

def IsDivSequence {α : Type u_1} {β : Type u_2} [Dvd α] [Dvd β] (f : α → β) : Prop

Alias of IsDvdSequence.

---

A function f : α → β is a divisibility sequence if a ∣ b implies f a ∣ f b.

Equations

• @IsDivSequence = @IsDvdSequence

theorem IsDvdSequence.id (α : Type u_1) [Dvd α] : IsDvdSequence id

theorem IsDvdSequence.const (α : Type u_1) {β : Type u_2} [Dvd α] [Monoid β] (b : β) : IsDvdSequence fun (x : α) => b

theorem IsDvdSequence.smul' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Dvd α] [Monoid β] [Monoid γ] {f : α → β} {g : α → γ} [SMul β γ] [IsScalarTower β γ γ] [IsScalarTower β β γ] [SMulCommClass β γ γ] (hf : IsDvdSequence f) (hg : IsDvdSequence g) : IsDvdSequence (f • g)

theorem IsDvdSequence.mul {α : Type u_1} {β : Type u_2} [Dvd α] [CommMonoid β] {f g : α → β} (hf : IsDvdSequence f) (hg : IsDvdSequence g) : IsDvdSequence (f * g)

theorem IsDvdSequence.smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Dvd α] [Monoid β] [Monoid γ] {f : α → γ} [SMul β γ] [IsScalarTower β γ γ] [IsScalarTower β β γ] [SMulCommClass β γ γ] (b : β) (hg : IsDvdSequence f) : IsDvdSequence (b • f)

theorem IsDvdSequence.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Dvd α] [Dvd β] [Dvd γ] {f : α → β} {g : β → γ} (hf : IsDvdSequence f) (hg : IsDvdSequence g) : IsDvdSequence (g ∘ f)

@[deprecated IsDvdSequence.smul (since := "2026-06-30")]

theorem IsDivSequence.smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Dvd α] [Monoid β] [Monoid γ] {f : α → γ} [SMul β γ] [IsScalarTower β γ γ] [IsScalarTower β β γ] [SMulCommClass β γ γ] (b : β) (hg : IsDvdSequence f) : IsDvdSequence (b • f)

Alias of IsDvdSequence.smul.

@[deprecated IsDvdSequence.id (since := "2026-06-30")]

theorem isDivSequence_id (α : Type u_1) [Dvd α] : IsDvdSequence id

Alias of IsDvdSequence.id.

def Nat.IsStrongDvdSequence (f : ℕ → ℕ) : Prop

A function f : ℕ → ℕ is a strong divisibility sequence if gcd (f a) (f b) = f (gcd a b).

Equations

• Nat.IsStrongDvdSequence f = ∀ (a b : ℕ), (f a).gcd (f b) = f (a.gcd b)

theorem Nat.IsStrongDvdSequence.isDvdSequence {f : ℕ → ℕ} (hf : IsStrongDvdSequence f) : IsDvdSequence f

theorem Nat.IsStrongDvdSequence.id : IsStrongDvdSequence id

theorem Nat.IsStrongDvdSequence.const (n : ℕ) : IsStrongDvdSequence fun (x : ℕ) => n