Revision #1453 → #1777 · back to history
modifiedp-adic number (series form)f7795b4170bb
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | Mathlib defines `Padic` as the Cauchy-sequence completion of ℚ with respect to `padicNorm`, not as formal series of `a_i p^i`, so the series-form definition is not directly formalized. |
| status | — | partial |
modifiedp-adic integer9bbb8d80b022
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `PadicInt p := {x : ℚ_[p] // ‖x‖ ≤ 1}` directly formalizes p-adic integers as elements of ℚ_[p] with norm ≤ 1, equivalent to non-negative valuation. |
| status | — | formalized |
modifiedp-adic absolute value8b13d8acd61b
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | padicNorm |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNorm |
| note | — | `padicNorm p q` on ℚ and the lifted `padicNormE` / `Norm` instance on ℚ_[p] formalize the p-adic absolute value. |
| status | — | formalized |
modifiedUnique p-adic series representation of rationals870577f2f8b5
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No theorem in Mathlib states that every rational is uniquely a convergent p-adic series of digits in {0,…,p−1}; only Cauchy-sequence representatives and approximations via `appr` exist. |
| status | — | not_formalized |
modifiedReduction mod p is not injective6053f8a361e1
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No specific statement in Mathlib formalizes 'reduction mod p loses information' as a motivational fact for p-adics. |
| status | — | not_formalized |
modifiedp-adic numbers form a fieldca4927edbd5f
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | `Padic p` is declared with `deriving … Field` (line 533 of PadicNumbers.lean), so ℚ_[p] is a field instance in Mathlib. |
| status | — | formalized |
modifiedp-adic integers as base-p expansions527aa8cb9e39
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib does not define `PadicInt` via formal base-p digit expansions; only the `appr` function gives finite truncations as natural numbers. |
| status | — | not_formalized |
modifiedRing of p-adic integers5cbc0601f921
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.instCommRing |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `instance instCommRing : CommRing ℤ_[p]` (line 92) directly establishes the ring structure on p-adic integers. |
| status | — | formalized |
modifiedp-adic number as p-adic integer with finitely many fractional digits36b109817d6b
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.isFractionRing |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | Mathlib proves `ℚ_[p]` is the fraction ring of `ℤ_[p]` (`PadicInt.isFractionRing`), formalizing the algebraic content of 'p-adic numbers are p-adic integers with finitely many fractional digits' without the digit-expansion form. |
| status | — | partial |
modifiedp-adic numbers form a field011cc22ffa79
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | Same as the Motivation field statement: `Padic p` derives `Field` in PadicNumbers.lean. |
| status | — | formalized |
modified1/5 as a 3-adic integere14bfbd34c4a
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No specific example in Mathlib establishes 1/5 as a 3-adic integer, though it follows from `PadicInt.isUnit_den` applied to a representative. |
| status | — | not_formalized |
modifiedp-adic integer as compatible sequence of residuesba9b0c64acbb
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.toZModPow |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.NumberTheory.Padics.RingHoms |
| note | — | Mathlib provides the compatible system of maps `PadicInt.toZModPow n : ℤ_[p] →+* ZMod (p^n)` and a universal `lift`, but does not define `ℤ_[p]` itself as a compatible-residue sequence. |
| status | — | partial |
modifiedEquivalence of base-p and residue definitions19c9e1a372d0
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Since Mathlib never sets up the base-p digit definition, no equivalence proof between digit and residue definitions exists. |
| status | — | not_formalized |
modified1/5 as 3-adic integer via residuesc868f039e516
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No worked example computing the 3-adic expansion of 1/5 via inverses mod 3^k exists in Mathlib. |
| status | — | not_formalized |
modifiedp-adic integer (formal power series)4b46a3341690
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib's `PadicInt` is the unit ball in ℚ_[p], not a formal power series ring with digit coefficients in {0,…,p−1}. |
| status | — | not_formalized |
modifiedp-adic unit1bd555042d33
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.isUnit_iff |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `PadicInt.isUnit_iff` characterizes units of ℤ_[p] as elements of norm 1, equivalent (via `toZMod`) to having nonzero leading digit. |
| status | — | formalized |
modifiedp-adic number (formal Laurent series)1acb32399f36
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib's ℚ_[p] is a Cauchy completion of ℚ, not a formal Laurent series construction. |
| status | — | not_formalized |
modifiedp-adic valuation8ca925d43146
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic.valuation |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | `Padic.valuation : ℚ_[p] → ℤ` (line 1040) gives the p-adic valuation; `padicValRat`, `padicValInt`, `padicValNat` provide it on ℚ/ℤ/ℕ. |
| status | — | formalized |
modifiedField of p-adic numbersf638e58bc250
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | `Padic p` is given a `Field` instance via the `deriving` clause in its definition. |
| status | — | formalized |
modifiedFactorization lemma for rationals3efd5e98da8e
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | padicValRat |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicVal.Basic |
| note | — | Mathlib has `padicValRat` and many divisibility lemmas implying the factorization r = p^v · m/n with p coprime to mn, but no single named lemma packages the canonical factorization. |
| status | — | partial |
modifiedp-adic valuation of a rational0d405f6d48b7
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | padicValRat |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicVal.Basic |
| note | — | `padicValRat p q : ℤ` directly formalizes the p-adic valuation of a rational number. |
| status | — | formalized |
modifiedp-adic series8e00e9a1322b
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib uses Cauchy sequences (`PadicSeq`) rather than formal Laurent series in p with integer coefficients; no `PadicSeries` type exists. |
| status | — | not_formalized |
modifiedEquivalence of p-adic series4a0849eadc4c
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Since p-adic series are not defined, neither is the equivalence relation between them; Mathlib instead uses CauSeq equivalence under `padicNorm`. |
| status | — | not_formalized |
modifiedNormalized p-adic seriesfe9e4910cd70
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No notion of 'normalized p-adic series' (with digits in {0,…,p−1}) exists in Mathlib. |
| status | — | not_formalized |
modifiedUniqueness of normalized series066a7266e27f
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Without a notion of normalized series, the uniqueness theorem is not formalized. |
| status | — | not_formalized |
modifiedSeries operations compatible with equivalence2b2e0b25a5ab
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Operations on p-adic series and their compatibility with equivalence are not formalized in Mathlib. |
| status | — | not_formalized |
modifiedp-adic numbers as equivalence classes03925399eae3
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | Mathlib defines ℚ_[p] as equivalence classes of `PadicSeq p` (Cauchy sequences of rationals under `padicNorm`), morally equivalent but not via formal series. |
| status | — | partial |
modifiedp-adic absolute value (equivalence-class form)22ca6e8763e0
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | padicNormE |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | `padicNormE` and the norm instance on ℚ_[p] are defined as |x|_p = p^(-v(x)), formalizing the absolute value via the valuation. |
| status | — | formalized |
modifiedField of p-adic numbers (via normalized series)e96314991d8e
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | Mathlib's `Padic p` is the field of p-adic numbers (constructed differently from normalized series). |
| status | — | formalized |
modifiedUnique homomorphism from rationals to p-adics8d044ec46ee8
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic.denseRange_ratCast |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | The rational embedding `Rat.cast : ℚ → ℚ_[p]` exists with dense range and is a ring hom; uniqueness from ℚ follows from `Rat`'s initial-field property but no named lemma states it explicitly for ℚ_[p]. |
| status | — | partial |
modifiedValuation as discrete valuation8c77140d253d
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.instIsDiscreteValuationRing |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `instance : IsDiscreteValuationRing ℤ_[p]` (line 521) formalizes that the p-adic valuation is a discrete valuation. |
| status | — | formalized |
modifiedDivision step for p-adic expansion395b57923c5b
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The explicit division-step algorithm for p-adic expansions of rationals is not formalized. |
| status | — | not_formalized |
modifiedComputing a via modular inversebbf5642786df
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No formalization of computing p-adic digits via modular inverses is present in Mathlib. |
| status | — | not_formalized |
modifiedp-adic expansion is eventually periodic iff rationalb9f3ff47db25
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The 'eventually periodic iff rational' characterization of p-adic expansions is not formalized. |
| status | — | not_formalized |
modified5-adic expansion computation8bfe92b8a2ff
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No specific worked example computing a 5-adic expansion is in Mathlib. |
| status | — | not_formalized |
modifiedp-adic integers as nonnegative-valuation p-adics83273c62d9f2
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `PadicInt p := {x : ℚ_[p] // ‖x‖ ≤ 1}` is equivalent to nonnegative valuation, with `valuation_coe_nonneg` providing the link. |
| status | — | formalized |
modifiedRationals that are p-adic integersc520993644e1
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.isUnit_den |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `PadicInt.isUnit_den` shows that a rational r has ‖r‖_p ≤ 1 iff its denominator is a p-adic unit (i.e., not divisible by p), exactly the rationals that are p-adic integers. |
| status | — | formalized |
modifiedZ_p is an integral domain13834b3d6079
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.instIsDomain |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `instance : IsDomain ℤ_[p]` (line 204) directly establishes that ℤ_[p] is an integral domain. |
| status | — | formalized |
modifiedUnits of Z_peade28d2ff68
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.isUnit_iff |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `PadicInt.isUnit_iff : IsUnit z ↔ ‖z‖ = 1` characterizes the units of ℤ_[p] as norm-1 elements. |
| status | — | formalized |
modifiedZ_p is a principal ideal domain820ed98f1e4b
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.ideal_eq_span_pow_p |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `PadicInt.ideal_eq_span_pow_p` shows every nonzero ideal is `span {p^n}`; together with the DVR instance this gives the PID structure. |
| status | — | formalized |
modifiedZ_p is a local ring of Krull dimension one4c2dd5029cb6
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.instIsLocalRing |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `instance : IsLocalRing ℤ_[p]` (line 499) formalizes the local-ring part; Krull dimension one follows from the DVR instance but no explicit `krullDim = 1` statement was located. |
| status | — | partial |
modifiedZ_p is a discrete valuation ring7d3b6d67bdab
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.instIsDiscreteValuationRing |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicIntegers |
| note | — | `instance : IsDiscreteValuationRing ℤ_[p]` (line 521) establishes the DVR structure. |
| status | — | formalized |
modifiedZ_p as completion of localization0f172812672f
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.adicCompletionIntegersEquiv |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.NumberTheory.Padics.HeightOneSpectrum |
| note | — | `PadicInt.adicCompletionIntegersEquiv` and `IsAdicComplete (maximalIdeal ℤ_[p]) ℤ_[p]` together encode that ℤ_[p] is the (p)-adic completion of ℤ_(p) / ℤ, matching the textbook statement. |
| status | — | partial |
modifiedp-adic absolute value via valuation7a58b65a1f9c
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic.norm_eq_zpow_neg_valuation |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | `Padic.norm_eq_zpow_neg_valuation` proves ‖x‖ = p^(-valuation x) for nonzero x ∈ ℚ_[p]. |
| status | — | formalized |
modifiedStrong triangle inequalityf176d03964db
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic.nonarchimedean |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | `Padic.nonarchimedean : ‖q + r‖ ≤ max ‖q‖ ‖r‖` (line 839) directly states the strong triangle inequality. |
| status | — | formalized |
modifiedp-adic distance and ultrametriccc62fb37c1ff
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic.instIsUltrametricDist |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | `instance : IsUltrametricDist ℚ_[p]` (line 781) plus `MetricSpace ℚ_[p]` formalize the ultrametric structure. |
| status | — | formalized |
modifiedQ_p as completion of Q42847a9bdcf4
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | By definition `Padic p := CauSeq.Completion.Cauchy (padicNorm p)`, together with `Padic.rat_dense` and `CompleteSpace ℚ_[p]`, formalizing the completion property. |
| status | — | formalized |
modifiedOpen balls equal closed balls7d5207750f79
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | IsUltrametricDist |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Topology.MetricSpace.Ultra.Basic |
| note | — | General ultrametric facts about clopen balls live in `IsUltrametricDist` API, which applies to ℚ_[p] via its `IsUltrametricDist` instance; no Padic-specific 'open = closed ball' lemma was found. |
| status | — | partial |
modifiedQ_p locally compact, Z_p compacte32cc573cc9e
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.compactSpace |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.ProperSpace |
| note | — | `PadicInt.compactSpace : CompactSpace ℤ_[p]` plus `instance : ProperSpace ℚ_[p]` (giving local compactness) formalize both claims. |
| status | — | formalized |
modifiedZ_p homeomorphic to Cantor setee714ec76441
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No homeomorphism between ℤ_[2] and the Cantor set is established in Mathlib. |
| status | — | not_formalized |
modifiedPontryagin dual of Z_p794ca33cca29
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has no PrüferGroup type and no theorem identifying the Pontryagin dual of ℤ_[p] with the Prüfer p-group. |
| status | — | not_formalized |
modifiedZ_p / p^n Z_p ≅ Z/p^n Zad3f86b00219
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.ker_toZModPow |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.RingHoms |
| note | — | `PadicInt.toZModPow n : ℤ_[p] →+* ZMod (p^n)` with `ker_toZModPow` showing the kernel is `span {p^n}` formalizes the isomorphism ℤ_[p]/p^n ≅ ℤ/p^nℤ. |
| status | — | formalized |
modifiedInverse limit of Z/p^n0c2d6109ec47
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.lift |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.NumberTheory.Padics.RingHoms |
| note | — | Mathlib does not name the inverse limit of `ZMod (p^n)` explicitly, but `PadicInt.lift` proves ℤ_[p] satisfies the universal property of that inverse limit. |
| status | — | partial |
modifiedZ_p as inverse limitfcfaf78a2c93
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.lift_unique |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.RingHoms |
| note | — | `PadicInt.lift_unique` shows ℤ_[p] is the universal/limit ring for compatible systems of `ZMod (p^n)`-valued ring homs, formalizing 'ℤ_[p] = lim ZMod (p^n)'. |
| status | — | partial |
modifiedNewton's method for p-adic inverse964747d49d04
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Newton's-method procedure for computing p-adic inverses is formalized in Mathlib. |
| status | — | not_formalized |
modifiedNewton's method for p-adic square root0668d1e70fd8
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Newton's-method computation of p-adic square roots is formalized. |
| status | — | not_formalized |
modifiedHensel lifting of polynomial factorizationde364a39be52
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | hensels_lemma |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.NumberTheory.Padics.Hensel |
| note | — | `hensels_lemma` lifts approximate roots in ℤ_[p] to exact ones (root form of Hensel), but the factorization form of Hensel lifting is not formalized as a separate theorem. |
| status | — | partial |
modifiedCardinality of Q_p and Z_p709d63162aad
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No theorem stating `#ℚ_[p] = 𝔠` or `#ℤ_[p] = 𝔠` was found in Mathlib (loogle returns 0 hits for Padic ∩ cardinal). |
| status | — | not_formalized |
modifiedQ_p has characteristic 0f8f816cd86f5
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | Padic.instCharZero |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.PadicNumbers |
| note | — | `instance : CharZero ℚ_[p]` (line 563) directly establishes characteristic 0. |
| status | — | formalized |
modifiedQ_p not orderable1d7ea77ace74
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No statement that ℚ_[p] cannot be linearly ordered as a field was found. |
| status | — | not_formalized |
modifiedAlgebraic closure of Q_p has infinite degree31b6a154fbe7
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No theorem about the degree (infinite) of the algebraic closure of ℚ_[p] is present; only the existence of `PadicAlgCl p` is formalized. |
| status | — | not_formalized |
modifiedC_p is algebraically closed969553fb7ca2
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicComplex.isAlgClosed |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.Complex |
| note | — | `instance isAlgClosed : IsAlgClosed ℂ_[p]` (line 244) directly formalizes that ℂ_[p] is algebraically closed. |
| status | — | formalized |
modifiedC_p not locally compact285229954b87
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No theorem stating ℂ_[p] is not locally compact was found. |
| status | — | not_formalized |
modifiedC_p isomorphic to C75a3b9152055
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The (noncanonical, AC-dependent) isomorphism ℂ_[p] ≅ ℂ is not formalized. |
| status | — | not_formalized |
modifiedAbsolute Galois group prosolvableb478202248fe
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No statement about the absolute Galois group of ℚ_[p] being prosolvable (Iwasawa) is formalized. |
| status | — | not_formalized |
modifiedTorsion subgroup of Q_p*5c9915023fb6
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No theorem identifying the torsion subgroup of ℚ_[p]^× (e.g., as (p−1)-th roots of unity for odd p) is formalized. |
| status | — | not_formalized |
modifiedCyclotomic subfields of Q_pfaa2ff810974
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No statement classifying cyclotomic subfields inside ℚ_[p] is present. |
| status | — | not_formalized |
modifiedFinite index of k-th powers24587953cea3
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No theorem about the finite index of (ℚ_[p]^×)^k in ℚ_[p]^× is present. |
| status | — | not_formalized |
modifiedHasse's local–global principle0f4b749c37e7
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Hasse–Minkowski / local-global principle is not formalized in Mathlib (no matches for Hasse-Minkowski). |
| status | — | not_formalized |
modifiedMahler's theorem900c391a9cc3
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | PadicInt.hasSum_mahler |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.NumberTheory.Padics.MahlerBasis |
| note | — | `PadicInt.hasSum_mahler` and the isometric equivalence `PadicInt.mahlerEquiv` together state Mahler's theorem in Mathlib. |
| status | — | formalized |
modifiedCompletion of Dedekind domain at primed4ca8522feaa
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | IsDedekindDomain.HeightOneSpectrum.adicCompletion |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.DedekindDomain.AdicValuation |
| note | — | Mathlib formalizes the adic completion of a Dedekind domain at a height-one prime via `IsDedekindDomain.HeightOneSpectrum.adicCompletion`, used in `Padic.adicCompletionEquiv` to recover ℚ_[p]. |
| status | — | formalized |
modifiedOstrowski's theorem for number fields154de19087de
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Ostrowski's theorem (classifying absolute values on number fields) does not appear to be formalized in Mathlib. |
| status | — | not_formalized |
modifiedp-adic solenoids02b7f51ccdec
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | p-adic solenoids are not defined in Mathlib. |
| status | — | not_formalized |
modifiedProfinite integers354506514f61
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Profinite integers (Ẑ) are not defined as a named object in Mathlib. |
| status | — | not_formalized |
modifiedn-adic integers via Chinese remainder theorem7315cb014bf9
| Field | From #1453 | To #1777 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No 'n-adic integer' construction with CRT-decomposition into products of ℤ_[p_i] is formalized. |
| status | — | not_formalized |
addedHensel's lemma lifts solutions mod p to higher prime powersac25a017f575
addedQuote notation for p-adic rationals24b7d414d073
addedTeichmüller representatives as p-adic digitsc7a2fda8241d
addedR has a unique proper algebraic extension51639c2c320c
addedComplex p-adic numbers C_p05176684642c
addedVolkenborn integral391cc05b4d3f
addedp-adic Hodge theory670d78ecc6be
addedp-adic Teichmüller theory01ac076d8315
addedp-adic quantum mechanicsba95f0effe72
addedAdele rings and idele groups6163d4a14518