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 functionfis a divisibility sequence ifa ∣ bimpliesf a ∣ f b.Nat.IsStrongDvdSeq: A functionf : ℕ → ℕis a strong divisibility sequence iffsatisfiesgcd (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)
:
@[deprecated IsDvdSequence (since := "2026-06-30")]
Alias of IsDvdSequence.
A function f : α → β is a divisibility sequence if a ∣ b implies f a ∣ f b.
Equations
Instances For
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)
@[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")]
Alias of IsDvdSequence.id.