Revision #1296 → #1976 · back to history
modifiedEuler's multi-valued functions5bb89614505f
| Field | From #1296 | To #1976 |
|---|
| mathlib.module | Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain | Mathlib.Analysis.Calculus.Implicit |
modifiedRussell's descriptive function3c00968dd253
| Field | From #1296 | To #1976 |
|---|
| mathlib.module | — | Mathlib.Logic.ExistsUnique |
modifiedHilbert's logical ε-function6567accd30eb
| Field | From #1296 | To #1976 |
|---|
| mathlib.module | — | Init.Classical |
addedμ-recursive functions57812a7045ff
addedTuring machinesf2e9f840caa9
modifiedTuring's unsolvability resultd6825e95ff2c
| Field | From #1296 | To #1976 |
|---|
| mathlib.decl | halting_problem | ComputablePred.halting_problem |
| note | The unsolvability of the Entscheidungsproblem is captured by the formalized non-computability of the halting problem (`halting_problem`), together with Rice's theorem. | The unsolvability of the Entscheidungsproblem is captured by the formalized non-computability of the halting problem (`ComputablePred.halting_problem`), together with Rice's theorem. |
modifiedRussell's ordered couple with sense96f009000681
| Field | From #1296 | To #1976 |
|---|
| mathlib.module | — | Init.Prelude |
addedCartesian product E × F6fbda845a9f2