Revision #1219 → #2027 · back to history
modifiedComplex numbers over reals638aee34b1a8
| Field | From #1219 | To #2027 |
|---|
| mathlib.decl | Complex.instAlgebra | Complex.instAlgebraOfReal |
| mathlib.module | Mathlib.Data.Complex.Module | Mathlib.LinearAlgebra.Complex.Module |
| note | Mathlib provides the ℝ-algebra (hence field extension) structure on ℂ. | Mathlib provides the ℝ-algebra (hence field extension) structure on ℂ via `Complex.instAlgebraOfReal`. |
modifiedRationals as subfield60f151a817a6
| Field | From #1219 | To #2027 |
|---|
| mathlib.decl | Rat.instAlgebraReal | DivisionRing.toRatAlgebra |
| mathlib.match_kind | exact | generalization |
| mathlib.module | Mathlib.Data.Real.Basic | Mathlib.Algebra.Algebra.Rat |
| note | Mathlib gives ℚ as a subfield/subring of ℝ via the canonical (injective) algebraMap. | `DivisionRing.toRatAlgebra` gives ℝ (any char-zero division ring) a canonical ℚ-algebra structure with injective `algebraMap`. |
modifiedDegree of extensionf3b963f72cdf
| Field | From #1219 | To #2027 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.Dimension.Free | Mathlib.LinearAlgebra.Dimension.Finrank |
modifiedMultiplicativity of degree04ab052c29f6
| Field | From #1219 | To #2027 |
|---|
| anchor.snippet | the extension | is finite if and only if both |
| note | States `finrank F K * finrank K A = finrank F A`, the tower law. | States `finrank F K * finrank K A = finrank F A`, the tower law. (Anchor tightened from generic 'the extension' for uniqueness.) |
| provenance | ai | ai-moderated |
modifiedRing homomorphisms between fields are injective02965871ad17
| Field | From #1219 | To #2027 |
|---|
| mathlib.module | Mathlib.Algebra.Field.Basic | Mathlib.RingTheory.SimpleRing.Basic |
modifiedC over R over Qf6b5a15fa63a
| Field | From #1219 | To #2027 |
|---|
| mathlib.decl | Complex.instAlgebra | Complex.instAlgebraOfReal |
| mathlib.module | Mathlib.Data.Complex.Module | Mathlib.LinearAlgebra.Complex.Module |
| note | ℂ/ℝ/ℚ tower is fully populated via existing `Algebra` and `IsScalarTower` instances. | ℂ/ℝ/ℚ tower is fully populated via `Complex.instAlgebraOfReal` plus `DivisionRing.toRatAlgebra` and `IsScalarTower` instances. |
modifiedAlgebraic iff simple extension finite5939d7ebfbbe
| Field | From #1219 | To #2027 |
|---|
| mathlib.module | Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra | Mathlib.FieldTheory.IntermediateField.Adjoin.Basic |
modifiedSimple algebraic iff finite6e72a4a87a5b
| Field | From #1219 | To #2027 |
|---|
| mathlib.module | Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra | Mathlib.FieldTheory.IntermediateField.Adjoin.Basic |
addedEvery finite extension is algebraic61c30a66cbf8
modifiedPurely transcendental extension exampledf939ad7b3a3
| Field | From #1219 | To #2027 |
|---|
| mathlib.decl | MvRatFunc | MvRatFunc.rank_eq_max_lift |
| note | Multivariate rational function fields exist (`MvRatFunc`), but the concept of "purely transcendental example" is not packaged as a named lemma. | Multivariate rational function fields exist (`FractionRing (MvPolynomial σ F)`) with rank results, but no named lemma packages the purely transcendental example. |
addedNormal closure61a6fdcaf6ad
modifiedFundamental theorem of Galois theory2bdfda6ffd05
| Field | From #1219 | To #2027 |
|---|
| mathlib.module | Mathlib.FieldTheory.Galois.IsGaloisGroup | Mathlib.FieldTheory.Galois.Basic |
addedQuaternions as CSA over reals5e84b32380c8
addedBrauer equivalence / Brauer group70a9aaa520aa
modifiedExtension of scalars by complexificationa16cfdf526fd
| Field | From #1219 | To #2027 |
|---|
| mathlib.decl | TensorProduct.instAlgebra | Algebra.TensorProduct.instAlgebra |
| note | Mathlib formalizes extension of scalars/base change as `TensorProduct R S M` with full algebra structure; complexification is the special case S = ℂ. | Mathlib formalizes extension of scalars/base change as `Algebra.TensorProduct.instAlgebra` on `R ⊗[S] T`; complexification is the special case S = ℂ. |