Revision #2413 → #3104 · back to history
addedRationals embed in any characteristic-zero field9855042d1c27
addedFinitely generated extension6b9f4fecbd59
addedFunction field of an algebraic variety21380b768812
modifiedMinimal polynomial is irreducible7089073575c5
| Field | From #2413 | To #3104 |
|---|
| mathlib.module | Mathlib.FieldTheory.Minpoly.Field | Mathlib.FieldTheory.Minpoly.Basic |
addedExistence of transcendence basisb910956e1848
addedTranscendence bases have equal cardinality805c0c716bf6
addedOnly finite extension of R is C (Frobenius)a6b21879a7ed
modifiedExtension of scalars by complexificationa16cfdf526fd
| Field | From #2413 | To #3104 |
|---|
| note | Mathlib formalizes extension of scalars/base change as `Algebra.TensorProduct.instAlgebra` on `R ⊗[S] T`; complexification is the special case S = ℂ. | Base change / extension of scalars is formalized via `Algebra.TensorProduct.instAlgebra` (the previous `Complexification` decl in `Mathlib.Analysis.NormedSpace.Complexification` does not exist). |
| provenance | ai | ai-moderated |