Revision #3543 → #4079 · back to history
modifiedSurreal numbers form a Field92e82a71e25e
| Field | From #3543 | To #4079 |
|---|
| mathlib.decl | Surreal | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.SetTheory.Surreal.Basic | — |
| note | `Surreal` is defined in Mathlib with a `LinearOrderedCommGroup`/field-like structure; being a proper class it is not a `Field` in the type-theoretic sense but the surreal number arithmetic satisfies the field axioms. | No `Surreal` declaration currently exists in Mathlib (verified via decl_exists and grep of `Mathlib/SetTheory`); the surreal numbers are not in the current Mathlib snapshot. |
| status | formalized | not_formalized |
modifiedNimbers form a Field6783db1ab18c
| Field | From #3543 | To #4079 |
|---|
| mathlib.decl | Nimber.instField | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.SetTheory.Nimber.Field | — |
| note | `Nimber` carries a `Field` instance (`Nimber.instField`) in `Mathlib/SetTheory/Nimber/Field.lean` via nim-addition and nim-multiplication. | No `Nimber` declaration currently exists in Mathlib (verified via decl_exists and grep); the nimbers are not in the current Mathlib snapshot. |
| status | formalized | not_formalized |
modifiedFermat's Last Theorem for regular primesa2c510a1bae7
| Field | From #3543 | To #4079 |
|---|
| mathlib.decl | FltRegular | — |
| mathlib.match_kind | generalization | — |
| mathlib.module | FltRegular | — |
| note | Kummer's proof of FLT for regular primes is not in core Mathlib; the FltRegular project (built on Mathlib) has formalized the Case I result. | Kummer's proof of FLT for regular primes is not in core Mathlib; the external FltRegular project has formalized Case I but is outside `Mathlib/`. |