Revision #1442 → #2109 · back to history
modifiedFifth-order Farey sequence3ae57e2e7291
| Field | From #1442 | To #2109 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Farey sequence definition found in Mathlib via grep or loogle. |
| status | — | not_formalized |
modifiedDecimal expansion of pi2e434a63d8b2
| Field | From #1442 | To #2109 |
|---|
| mathlib.decl | — | Real.pi |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic |
| note | — | Real.pi is defined in Mathlib but no decimal-digits sequence of pi is formalized. |
| status | — | partial |
modifiedTotient valence function2527574aa197
| Field | From #1442 | To #2109 |
|---|
| mathlib.decl | — | Nat.totient |
| mathlib.match_kind | — | — |
| mathlib.module | — | Mathlib.Data.Nat.Totient |
| note | — | Nat.totient is in Mathlib but the inverse-counting totient valence function is not. |
| status | — | partial |
modifiedLexicographical ordering of sample sequences63b308bc29c8
| Field | From #1442 | To #2109 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | This is an editorial ordering of OEIS sample sequences with no Mathlib counterpart. |
| status | — | not_formalized |
modifiedSelf-referential sequence A031135330356895b16
| Field | From #1442 | To #2109 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | This particular OEIS self-referential sequence is not in Mathlib. |
| status | — | not_formalized |
modifiedRussell's paradox for A053169a2c26ef68c55
| Field | From #1442 | To #2109 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | OEIS-meta paradox of sequence A053169 has no Mathlib formalization. |
| status | — | not_formalized |
modifiedCubes sequence A000578a5f96e395a9d
| Field | From #1442 | To #2109 |
|---|
| mathlib.decl | — | HPow.hPow |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The function n ↦ n^3 is expressible via standard power but no named A000578 sequence exists in Mathlib. |
| status | — | partial |
modifiedMultiplicative function keywordaa88d4d1a1fd
| Field | From #1442 | To #2109 |
|---|
| mathlib.decl | — | ArithmeticFunction.IsMultiplicative |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.ArithmeticFunction.Defs |
| note | — | Mathlib defines ArithmeticFunction.IsMultiplicative matching the OEIS multiplicative-function notion. |
| status | — | formalized |
modifiedLazy caterer's sequence offset91008b182688
| Field | From #1442 | To #2109 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No lazy-caterer or pancake-cut sequence found in Mathlib. |
| status | — | not_formalized |
modifiedSloane's gapa0a7054684fe
| Field | From #1442 | To #2109 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Sloane's gap is an empirical OEIS observation with no Mathlib formalization. |
| status | — | not_formalized |
addedMersenne primes A00066872b2c6ae0e1f
addedExactly fifteen supersingular primesad3c1bb16177
addedPascal's triangle A0073189ab1d490504e
addedMagic square smallest prime sequence A104157d93c4437f85a
addedMultiplicative computation in A0469701221dea0af4f