Revision #1830 → #2348 · back to history
modifiedFields are commutative rings with only ideals (0) and R012642a81612
| Field | From #1830 | To #2348 |
|---|
| mathlib.decl | Ideal.IsMaximal.isField | Ring.isField_iff_isSimpleOrder_ideal |
| mathlib.match_kind | generalization | exact |
| mathlib.module | Mathlib.RingTheory.Ideal.Quotient.Basic | Mathlib.RingTheory.Ideal.Basic |
| note | The equivalence between fields and commutative rings with exactly two ideals is captured via `Ideal.isField_iff_isMaximal` / `Ideal.IsMaximal` characterizations; the `(0)` maximal-ideal characterization gives this. | `Ring.isField_iff_isSimpleOrder_ideal : IsField R ↔ IsSimpleOrder (Ideal R)` is exactly the characterization via having precisely two ideals. |
modifiedDifferential field30e9830b8abf
| Field | From #1830 | To #2348 |
|---|
| mathlib.module | Mathlib.FieldTheory.Differential.Basic | Mathlib.RingTheory.Derivation.DifferentialRing |
| note | `Mathlib/FieldTheory/Differential/Basic.lean` formalizes fields equipped with a derivation. | Mathlib's `Differential` typeclass (in `Mathlib/RingTheory/Derivation/DifferentialRing.lean`) equips a ring/field with a derivation; the field-specific theory lives in `Mathlib/FieldTheory/Differential/`. |
addedCharacteristic p annihilates field elements0ef265c0ee66
addedComplex numbers as residue field R[X]/(X²+1)b845c501a0f3
addedTranscendence of e08979eea5cfa
addedAlgebraic number fieldae3715c1b62a