Commit 2026-06-30 18:26 c36598a9

View on Github →

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.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/DvdSequence.lean

added def IsDvdSequence

added theorem Nat.IsStrongDvdSequence.isDvdSequence

added def Nat.IsStrongDvdSequence

added theorem smul_dvd_smul

Modified Mathlib/Data/Nat/Fib/Basic.lean

deleted theorem Nat.fib_dvd

added theorem Nat.isDvdSequence_fib

added theorem Nat.isStrongDvdSequence_fib

Modified Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

deleted theorem IsDivSequence.smul

deleted def IsDivSequence

deleted theorem isDivSequence_id