Revision #3104 → #3610 · back to history
addedTower of extensions56230deca0d1
modifiedOnly finite extension of R is C (Frobenius)a6b21879a7ed
| Field | From #3104 | To #3610 |
|---|
| mathlib.decl | — | Real.nonempty_algEquiv_or |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Analysis.Complex.Polynomial.Basic |
| note | Frobenius's theorem that the only finite field extensions of ℝ are ℝ and ℂ is not (as of review) packaged in Mathlib. | `Real.nonempty_algEquiv_or` states every algebraic (hence finite) extension of ℝ is algebra-isomorphic to ℝ or ℂ, covering the Frobenius statement. |
| status | not_formalized | formalized |
modifiedAzumaya algebra274ae3c887ea
| Field | From #3104 | To #3610 |
|---|
| mathlib.decl | — | IsAzumaya |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Algebra.Azumaya.Defs |
| note | Azumaya algebras (CSA-analogue over commutative local rings) do not appear to have a dedicated definition in Mathlib at the time of review. | `IsAzumaya R A` in `Mathlib.Algebra.Azumaya.Defs` formalizes Azumaya algebras via bijectivity of the left-right multiplication map on a projective, faithful, finitely generated module. |
| status | not_formalized | formalized |