Field theory and polynomials
The Lean Pool projects whose card's first MSC2020 code is in class 12, Field theory and polynomials: 2 articles, one per card.
DefinitionThe Fundamental Inequality of Valued Fields#
Defines the ramification index and residue degree of an extension of valued fields and proves the fundamental inequality e * f ≤ finrank K L for finite extensions, via the valuation independence of products of coset representatives and residue-field basis lifts.
Quoted from the card LeanPool/projects/fundamental-inequality.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
Valuation.ramificationIndex(def; a main declaration), declared in LeanPool/FundamentalInequality.lean, line 74: “Defines the ramification index e(w/v) as the relative index of the value group of the restricted valuation inside the value group of the extension.”Valuation.residueDegree(def), declared in LeanPool/FundamentalInequality.lean, line 59: “Defines the residue degree f(w/v) as the rank of the residue field extension.”Valuation.valuation_independence(lemma), declared in LeanPool/FundamentalInequality.lean, line 206: “Elements with valuations in distinct cosets and residues that are linearly independent give products that are linearly independent over the base field.”Valuation.fundamentalInequality(theorem; a main declaration), declared in LeanPool/FundamentalInequality.lean, line 476: “The fundamental inequality e(w/v) * f(w/v) ≤ finrank K L for finite extensions of valued fields.” Its source, as the card gives it: “F.-V. Kuhlmann, Valued Fields, Chapter 4, §4.4.”
Project
- Authors: Alessandro Linzi.
- Source: Valued Fields by Franz-Viktor Kuhlmann.
- Project repository: linzialessandro/FundamentalInequality.
- Provenance: human, which in Lean Pool's terms means its Lean proofs were “written by people”.
- License: Apache-2.0.
- MSC2020: 12J20.
- In Lean Pool: LeanPool/FundamentalInequality, from the card LeanPool/projects/fundamental-inequality.yaml.
Sources
InstancePuiseux's theorem#
Constructs Puiseux series as the bounded-denominator subfield of rational-exponent Hahn series. Proves that this field is algebraic over Laurent series over any coefficient field, and is an algebraic closure when the coefficient field is algebraically closed of characteristic zero. The Newton-Puiseux proof includes reusable Hensel splitting and polynomial translation lemmas. Dean Cureton directed the AI formalization and subsequently simplified its proofs.
Quoted from the card LeanPool/projects/puiseux.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
PuiseuxSeries.isAlgClosure(instance; a main declaration), declared in LeanPool/Puiseux/AlgClosed.lean, line 436: “For an algebraically closed field K of characteristic zero, the field of Puiseux series over K is an algebraic closure of the Laurent series field K((t)).”PuiseuxSeries.isAlgebraic(instance), declared in LeanPool/Puiseux/Algebraic.lean, line 124: “Over any field K, the Puiseux series field is algebraic over the Laurent series field.”PuiseuxSeries.mem_subfield_iff_support(theorem), declared in LeanPool/Puiseux/Basic.lean, line 139: “A rational-exponent Hahn series belongs to the Puiseux subfield if and only if its support lies in (1/n) times the integers for some positive integer n.”Polynomial.Monic.exists_factorization_rootMultiplicity(theorem), declared in LeanPool/Puiseux/HenselSplitting.lean, line 116: “A monic degree-m polynomial over K[[t]] whose reduction has a root of multiplicity k, with 0 < k < m, factors into monic polynomials of degrees k and m-k.”
Project
- Authors: Dean Cureton.
- Source: Puiseux's theorem in Lean 4.
- Project repository: deancureton/Puiseux, at commit 73e78681.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 12F05, 13F25.
- In Lean Pool: LeanPool/Puiseux, from the card LeanPool/projects/puiseux.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.