Commit 2024-05-22 16:39 89a94ada

View on Github →

feat(NumberTheory/EllipticDivisibilitySequence): define recursion principle for normalised EDS (#10843) ... and make implicit variables in Data.Nat.EvenOddRec consistent.

Estimated changes

Modified Mathlib/Data/Int/Defs.lean

Modified Mathlib/Data/Nat/EvenOddRec.lean

modified theorem Nat.evenOddRec_even

modified theorem Nat.evenOddRec_odd

modified theorem Nat.evenOddRec_zero

Modified Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

added theorem IsDivSequence.smul

modified def IsDivSequence

deleted theorem IsDivSequence_id

deleted theorem IsDivSequence_mul

added theorem IsEllDivSequence.smul

modified def IsEllDivSequence

deleted theorem IsEllDivSequence_id

deleted theorem IsEllDivSequence_mul

added theorem IsEllSequence.smul

modified def IsEllSequence

deleted theorem IsEllSequence_id

deleted theorem IsEllSequence_mul

added theorem isDivSequence_id

added theorem isEllDivSequence_id

added theorem isEllSequence_id