Revision #1435 → #1776 · back to history
modifiedIntegers85a2783c984e
| Field | From #1435 | To #1776 |
|---|
| mathlib.module | — | Init.Data.Int.Basic |
| note | The integer type `Int` (`ℤ`) is a Lean core definition used throughout Mathlib. | The integer type `Int` (`ℤ`) is a Lean core inductive used throughout Mathlib. |
modifiedPythagorean triples (Plimpton 322)18a346d2e6c7
| Field | From #1435 | To #1776 |
|---|
| anchors | [{"section":"History","snippet":"a list of Pythagorean triples , that is, integers"},{"type":"math_alttext","value":"{\\displaystyle \\left({\\frac {1}{2}}\\left(x-{\\frac {1}{x}}\\right)\\right)^{2}+1=\\left({\\frac {1}{2}}\\left(x+{\\frac {1}{x}}\\right)\\right)^{2},}"}] | — |
modifiedMultiplication873eed4a138d
| Field | From #1435 | To #1776 |
|---|
| mathlib.module | — | Init.Prelude |
modifiedDivisibilitya93b55afbf30
| Field | From #1435 | To #1776 |
|---|
| mathlib.module | — | Init.Prelude |
modifiedEuclid's division lemma619214cd08be
| Field | From #1435 | To #1776 |
|---|
| mathlib.module | — | Init.Data.Nat.Div.Basic |
modifiedGreatest common divisor80990632a2eb
| Field | From #1435 | To #1776 |
|---|
| mathlib.module | — | Init.Data.Nat.Gcd |
modifiedCoprime integersce5318d8ad74
| Field | From #1435 | To #1776 |
|---|
| mathlib.module | — | Init.Data.Nat.Coprime |
modifiedModular arithmetic27eac4e7c27b
| Field | From #1435 | To #1776 |
|---|
| anchors | [{"section":"Elementary number theory","snippet":"Modular arithmetic works with finite sets of integers"},{"type":"math_alttext","value":"{\\displaystyle a^{\\varphi (n)}\\equiv 1{\\pmod {n}},}"}] | — |
modifiedCongruence3a52b5bb5512
| Field | From #1435 | To #1776 |
|---|
| anchors | [{"section":"Elementary number theory","snippet":"A congruence of two integers"},{"type":"math_alttext","value":"{\\displaystyle a^{\\varphi (n)}\\equiv 1{\\pmod {n}},}"}] | — |
modifiedResidue class47b7fffdfccc
| Field | From #1435 | To #1776 |
|---|
| anchors | [{"section":"Elementary number theory","snippet":"is a set that contains all integers congruent to a specified"},{"type":"math_alttext","value":"{\\displaystyle a^{\\varphi (n)}\\equiv 1{\\pmod {n}},}"}] | — |
modifiedFermat's little theorem842270911a23
| Field | From #1435 | To #1776 |
|---|
| anchors | [{"section":"Elementary number theory","snippet":"An influential theorem is Fermat's little theorem"},{"type":"math_alttext","value":"{\\displaystyle a^{\\varphi (n)}\\equiv 1{\\pmod {n}},}"}] | — |
modifiedEuler's theorem87ecd818ac7e
| Field | From #1435 | To #1776 |
|---|
| anchors | [{"section":"Elementary number theory","snippet":"Euler's theorem extends this to assert that every integer"},{"type":"math_alttext","value":"{\\displaystyle a^{\\varphi (n)}\\equiv 1{\\pmod {n}},}"}] | — |
modifiedAnalysis (limit)0971b594b4d3
| Field | From #1435 | To #1776 |
|---|
| mathlib.module | Mathlib.Order.Filter.Basic | Mathlib.Order.Filter.Defs |
modifiedLimit of a sequence0c09a3ee9622
| Field | From #1435 | To #1776 |
|---|
| mathlib.module | Mathlib.Order.Filter.Basic | Mathlib.Order.Filter.Defs |
modifiedRiemann zeta functiond288cb52faee
| Field | From #1435 | To #1776 |
|---|
| anchors | [{"section":"Analytic number theory","snippet":"It is defined as the series"},{"type":"math_alttext","value":"{\\displaystyle \\zeta (s)=\\sum _{n=1}^{\\infty }{\\frac {1}{n^{s}}}={\\frac {1}{1^{s}}}+{\\frac {1}{2^{s}}}+{\\frac {1}{3^{s}}}+\\cdots }"},{"type":"math_alttext","value":"{\\displaystyle \\zeta (s)=\\prod _{p{\\text{ prime}}}\\left(1-{\\frac {1}{p^{s}}}\\right)^{-1}.}"}] | — |
modifiedEuler product formulafdadc88f5ab2
| Field | From #1435 | To #1776 |
|---|
| anchors | [{"section":"Analytic number theory","snippet":"Euler demonstrated a link involving the infinite product over all prime numbers"},{"type":"math_alttext","value":"{\\displaystyle \\zeta (s)=\\sum _{n=1}^{\\infty }{\\frac {1}{n^{s}}}={\\frac {1}{1^{s}}}+{\\frac {1}{2^{s}}}+{\\frac {1}{3^{s}}}+\\cdots }"},{"type":"math_alttext","value":"{\\displaystyle \\zeta (s)=\\prod _{p{\\text{ prime}}}\\left(1-{\\frac {1}{p^{s}}}\\right)^{-1}.}"}] | — |
modifiedRiemann hypothesis1517b39eaeeb
| Field | From #1435 | To #1776 |
|---|
| anchors | [{"section":"Analytic number theory","snippet":"Riemann extended the definition to a complex variable and conjectured"},{"type":"math_alttext","value":"{\\displaystyle \\zeta (s)=\\sum _{n=1}^{\\infty }{\\frac {1}{n^{s}}}={\\frac {1}{1^{s}}}+{\\frac {1}{2^{s}}}+{\\frac {1}{3^{s}}}+\\cdots }"},{"type":"math_alttext","value":"{\\displaystyle \\zeta (s)=\\prod _{p{\\text{ prime}}}\\left(1-{\\frac {1}{p^{s}}}\\right)^{-1}.}"}] | — |
modifiedDedekind zeta functionsc54d927f9bd9
| Field | From #1435 | To #1776 |
|---|
| mathlib.decl | dedekindZeta | NumberField.dedekindZeta |
| note | `dedekindZeta` defines the Dedekind zeta function of a number field. | `NumberField.dedekindZeta K s` defines the Dedekind zeta function of a number field. |
modifiedDiophantine approximation5f8a38dccf6c
| Field | From #1435 | To #1776 |
|---|
| mathlib.decl | Real.exists_rat_abs_sub_lt_one_div_den_sq_of_irrational | Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational |
addedFermat's Last Theorem98b7f0709117
addedGoldbach's conjecture14d7297c5642
addedChinese remainder theorem1fb1f1ad09fa
addedPell equation66dd6c70d3a1
addedWilson's theorembce5ee046461
addedLagrange's four-square theoreme81eb1668672
addedQuadratic reciprocityc3b5cd367743
addedDirichlet's theorem on arithmetic progressionse8ccab8291a3
addedEuler's totient functione4cb8bf11f9c
addedPerfect numberbf291956c043
addedDivisor function4a2e9fcd95e6
addedTwin prime conjecturef2c2cdb0912d
addedWaring's problem225de9688b63