Revision #1220 → #1830 · back to history
modifiedField (informal)6fa4572df04c
| Field | From #1220 | To #1830 |
|---|
| note | Same `Field` class captures the informal description. | The same `Field` class captures the informal description. |
modifiedField of rational numbersd4cf8d136ce1
| Field | From #1220 | To #1830 |
|---|
| mathlib.module | Mathlib.Data.Rat.Defs | Mathlib.Algebra.Field.Rat |
| note | Mathlib provides a `Field` instance on `ℚ`. | Mathlib provides a `Field` instance on `ℚ` via `Rat.instField`. |
modifiedNonzero elements form a multiplicative group21a2a9258ae8
| Field | From #1220 | To #1830 |
|---|
| mathlib.decl | DivisionRing.toGroupWithZero | DivisionSemiring.toGroupWithZero |
| note | Via `DivisionRing → GroupWithZero` (and commutativity from `Field`), nonzero elements form a commutative group; `Units K` packages this group. | Via `DivisionSemiring.toGroupWithZero` (and commutativity from `Field`), nonzero elements form a commutative group; `Units K` packages this group. |
addedFreshman's dream in characteristic p1627a6ebdf39
modifiedFinite fieldc354883ffd5a
| Field | From #1220 | To #1830 |
|---|
| mathlib.decl | FiniteField | FiniteField.card' |
| mathlib.match_kind | exact | invocation |
| note | Finite fields are formalized as `[Field K] [Fintype K]` with the `FiniteField` namespace collecting results. | There is no dedicated `FiniteField` typeclass; finite fields are encoded as `[Field K] [Fintype K]` and the `FiniteField` namespace collects results. |
| status | formalized | partial |
addedFields are commutative rings with only ideals (0) and R012642a81612
addedField of formal Laurent seriese75f05379335
modifiedCompositum of subfieldse34b818151de
| Field | From #1220 | To #1830 |
|---|
| mathlib.decl | IntermediateField.instSup | IntermediateField.sup_def |
| note | The compositum is realized as the `⊔` (sup) of intermediate fields (and similarly via `Subfield.closure`). | The compositum is realized as the `⊔` (sup) of intermediate fields, with `IntermediateField.sup_def` showing it equals `adjoin F (E ∪ E')`. |
modifiedField extensiond42c9584fd4b
| Field | From #1220 | To #1830 |
|---|
| mathlib.module | Mathlib.Algebra.Algebra.Basic | Mathlib.Algebra.Algebra.Defs |
modifiedDegree of a field extension701720d8c162
| Field | From #1220 | To #1830 |
|---|
| note | The degree `[F : E]` is `Module.finrank E F`; infinite-rank case is `Module.rank`. | The degree `[F : E]` is `Module.finrank E F`; the infinite-rank case is `Module.rank`. |
modifiedFinite extensions are algebraic7d771ecf0a99
| Field | From #1220 | To #1830 |
|---|
| mathlib.module | Mathlib.RingTheory.Algebraic.Basic | Mathlib.RingTheory.Algebraic.Integral |
| note | `Algebra.IsAlgebraic.of_finite` derives `IsAlgebraic` from a finite-dimensional extension. | `Algebra.IsAlgebraic.of_finite` is an instance deriving `IsAlgebraic` from a finite-dimensional extension. |
modifiedArtin–Schreier theorem (real closed fields)7a46961b860c
| Field | From #1220 | To #1830 |
|---|
| note | No general Artin–Schreier theorem on the degree of [F̄ : F] = 2 forcing F to be real closed appears in Mathlib (only the special case `Real.nonempty_algEquiv_or` for ℝ). | No general Artin–Schreier theorem on the degree of [F̄ : F] = 2 forcing F to be real closed appears in Mathlib (only the special case for ℝ). |
addedField of Puiseux seriesa38d0f10cd04
modifiedComplete implies Archimedeanbe41f67b0b39
| Field | From #1220 | To #1830 |
|---|
| note | Scoped instance derives `Archimedean` from `ConditionallyCompleteLinearOrderedField`. | A scoped instance derives `Archimedean` from `ConditionallyCompleteLinearOrderedField`. |
modifiedUniqueness of complete ordered field Rdd08577029d5
| Field | From #1220 | To #1830 |
|---|
| note | `inducedOrderRingIso`/`uniqueOrderRingIso` give a canonical (unique) order-ring isomorphism between any two conditionally complete linearly ordered fields. | `inducedOrderRingIso` gives a canonical (unique) order-ring isomorphism between any two conditionally complete linearly ordered fields. |
addedHyperreal numbers4a04a110a1d8
addedField of p-adic numbers6af3eca7bc2c
modifiedAx–Kochen theorem3db788950797
| Field | From #1220 | To #1830 |
|---|
| note | No Ax–Kochen theorem appears in Mathlib (grep for `AxKochen` finds nothing). | No Ax–Kochen theorem appears in Mathlib. |
modifiedGalois group393122c75c3e
| Field | From #1220 | To #1830 |
|---|
| note | `Gal(F/E)` is realized as `F ≃ₐ[E] F` (notation `Gal(F/K)` is used throughout `FieldTheory/Galois`). | `Gal(F/E)` is realized as `F ≃ₐ[E] F` (the `Gal(F/K)` notation is used throughout `FieldTheory/Galois`). |
modifiedFundamental theorem of Galois theory477bc532410a
| Field | From #1220 | To #1830 |
|---|
| mathlib.module | Mathlib.FieldTheory.Galois.IsGaloisGroup | Mathlib.FieldTheory.Galois.Basic |
modifiedAbel–Ruffini theorem4722f4eb193b
| Field | From #1220 | To #1830 |
|---|
| mathlib.decl | not_solvable_by_rad | isSolvable_gal_of_irreducible |
| mathlib.match_kind | exact | generalization |
| note | `Mathlib/FieldTheory/AbelRuffini.lean` formalizes the Abel–Ruffini theorem. | `Mathlib/FieldTheory/AbelRuffini.lean` formalizes only one direction (solvable-by-rad implies solvable Galois group); the existence of a non-solvable quintic lives in `Archive/Wiedijk100Theorems/AbelRuffini.lean`. |
| status | formalized | partial |
modifiedElementarily equivalent fields6ef2099d7d00
| Field | From #1220 | To #1830 |
|---|
| mathlib.module | Mathlib.ModelTheory.ElementaryMaps | Mathlib.ModelTheory.Semantics |
modifiedLefschetz principle4a8532794688
| Field | From #1220 | To #1830 |
|---|
| mathlib.decl | FirstOrder.Field.isComplete_ACF₀ | FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize |
| mathlib.match_kind | generalization | exact |
| note | Completeness of the theory ACF₀ is in Mathlib (`Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean`); the explicit Lefschetz statement comparing ℂ to other ACF₀ models is not isolated as a named theorem. | The Lefschetz principle is formalized as `FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize`, with completeness of ACF₀ from `FirstOrder.Field.ACF_isComplete`. |
| status | partial | formalized |
modifiedŁoś's theorem45d18f19acbb
| Field | From #1220 | To #1830 |
|---|
| mathlib.decl | FirstOrder.Language.Ultraproduct | FirstOrder.Language.Ultraproduct.sentence_realize |
| note | Łoś's theorem is formalized in `Mathlib/ModelTheory/Ultraproducts.lean`. | Łoś's theorem is formalized as `FirstOrder.Language.Ultraproduct.sentence_realize` in `Mathlib/ModelTheory/Ultraproducts.lean`. |
addedGalois group of finite extension of finite fielddc744fdd9c9c
addedBrauer group of a fieldd3512fdbb39b
modifiedUnique solution of ax = b in a field17443ecb8754
| Field | From #1220 | To #1830 |
|---|
| mathlib.module | Mathlib.Algebra.GroupWithZero.Basic | Mathlib.Algebra.GroupWithZero.Units.Basic |
addedEvery vector space has a basisa5cc2d8c12aa
modifiedField of functions8a2499393a61
| Field | From #1220 | To #1830 |
|---|
| mathlib.module | Mathlib.FieldTheory.RatFunc.Basic | Mathlib.FieldTheory.RatFunc.Defs |
modifiedHasse–Minkowski theoremab23d23abf3d
| Field | From #1220 | To #1830 |
|---|
| note | No Hasse–Minkowski theorem appears in Mathlib (grep finds no matches). | No Hasse–Minkowski theorem appears in Mathlib. |
modifiedKronecker–Weber theorem857e4bd4c4a7
| Field | From #1220 | To #1830 |
|---|
| note | Kronecker–Weber is not in Mathlib (no `KroneckerWeber` decl). | Kronecker–Weber is not in Mathlib. |
addedQuaternionse8d9cf0cbe74