Revision #1232 → #2793 · back to history
modifiedFormal seriesa75b04cf774c
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | HahnSeries |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.RingTheory.HahnSeries.Basic |
| note | — | No abstract `FormalSeries` in Mathlib; the most general realization is `HahnSeries`, with `PowerSeries`, `MvPowerSeries`, `LaurentSeries` as concrete instances. |
| status | — | partial |
modifiedFormal power series88963240bbed
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Basic |
| note | — | `PowerSeries R := MvPowerSeries Unit R` is the univariate formal power series type. |
| status | — | formalized |
modifiedRing of formal power series over Rec3906877b46
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Basic |
| note | — | `PowerSeries R` inherits the (semi)ring structure from `MvPowerSeries Unit R` (see `MvPowerSeries.instSemiring`). |
| status | — | formalized |
modifiedSeries with coefficients [1,-3,5,-7,...]e62fb172aef1
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Illustrative expository example, not a named object in Mathlib. |
| status | — | not_formalized |
modifiedSeries with factorial coefficients1a9bcd564428
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Expository example (∑ n! X^n); Mathlib has `PowerSeries.exp` (with 1/n!) but not this specific series. |
| status | — | not_formalized |
modifiedMultiplicative inverse of formal power series51ff57088b02
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.invOfUnit |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Inverse |
| note | — | `PowerSeries.invOfUnit` constructs the inverse when the constant term is a unit; `PowerSeries.inv` handles the field case. |
| status | — | formalized |
modifiedDivision of formal power series85cb14dc0f4b
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.inv |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Inverse |
| note | — | Division B/A is `B * A⁻¹` via `PowerSeries.inv`; a dedicated `Div` instance exists only via the `Field k⟦X⟧` inference over a field. |
| status | — | partial |
modifiedCoefficient extraction operator0a7dff49848b
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.coeff |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Basic |
| note | — | `PowerSeries.coeff (n : ℕ) : R⟦X⟧ →ₗ[R] R` extracts the n-th coefficient. |
| status | — | formalized |
modifiedRing of formal power series in X over Rdc628600d290
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Basic |
| note | — | The (semi)ring structure on `PowerSeries R` is provided by `MvPowerSeries.instSemiring` transported via `PowerSeries := MvPowerSeries Unit R`. |
| status | — | formalized |
modifiedFormal power series ring as completionf7d7b1d8cdd2
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib's `MvPowerSeries/Basic.lean` explicitly notes the I-adic completion characterization is not yet proved (TODO). |
| status | — | not_formalized |
modifiedAddition and multiplication of sequences (Cauchy product)9711bf2bc8cf
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.coeff_mul |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Basic |
| note | — | `coeff n (φ * ψ) = ∑ p ∈ antidiagonal n, coeff p.1 φ * coeff p.2 ψ` is exactly the Cauchy product. |
| status | — | formalized |
modifiedProduct topology on R^N598ee06d4cb7
| Field | From #1232 | To #2793 |
|---|
| anchor.snippet | We may give | the product topology , where each copy of |
| mathlib.decl | — | PowerSeries.WithPiTopology |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.PiTopology |
| note | — | Sharpened anchor: original snippet 'We may give' was too vague. |
| provenance | ai-agent1 | ai-moderated |
| status | — | formalized |
modifiedI-adic topologyd01e6793b272
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | Ideal.adicTopology |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology |
| note | — | `Ideal.adicTopology I` gives the I-adic topology for any ideal, but its equality with `WithPiTopology` on `R⟦X⟧` is not proved in Mathlib. |
| status | — | partial |
modifiedMetric on formal power series7c2331e6de17
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `MetricSpace (PowerSeries R)` instance in Mathlib; only the pi-topology / uniform structure is provided. |
| status | — | not_formalized |
modifiedConvergence iff terms tend to 02ef1d1e30e15
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean |
| note | — | General nonarchimedean-group version exists; specialization to `R⟦X⟧` is not stated explicitly. |
| status | — | partial |
modifiedInfinite product convergence7ee95f8a7fab
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | NonarchimedeanGroup.multipliable_iff_tendsto_cofinite_one |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean |
| note | — | General nonarchimedean-group version exists; specialization to `R⟦X⟧` is not stated. |
| status | — | partial |
modifiedUniversal property of formal power series ring6125359cbd3d
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | MvPowerSeries.aeval_unique |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.RingTheory.MvPowerSeries.Evaluation |
| note | — | `MvPowerSeries.aeval_unique` gives uniqueness of a continuous R-algebra hom sending X to a fixed value; the univariate specialization is `PowerSeries.aeval`. |
| status | — | partial |
modifiedn-th power of a formal power seriesbb64ec6abdf6
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.coeff_pow |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Basic |
| note | — | The Monoid structure gives `f^n`; `PowerSeries.coeff_pow` computes its coefficients. |
| status | — | formalized |
modifiedComplex powers of series with constant term 18a3cb3b0c824
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.binomialSeries |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Binomial |
| note | — | `binomialSeries` gives (1+X)^r for r in a binomial ring; general complex-power operator on 1+m·R⟦X⟧ is not packaged. |
| status | — | partial |
modifiedInvertibility criterionc6313747e3e7
| Field | From #1232 | To #2793 |
|---|
| anchor.snippet | is invertible in | is invertible in [MATH] if and only if its constant coefficient |
| mathlib.decl | — | PowerSeries.isUnit_iff_constantCoeff |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Inverse |
| note | — | Sharpened anchor to capture the iff criterion, though [MATH] placeholder remains in-source. |
| provenance | ai-agent1 | ai-moderated |
| status | — | formalized |
modifiedGeometric series formula34a41e2c70bb
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.mk_one_mul_one_sub_eq_one |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.WellKnown |
| note | — | `(1 + X + X² + …) · (1 − X) = 1`; also `PowerSeries.invUnitsSub` for 1/(u−X). |
| status | — | formalized |
modifiedDiscrete valuation ring over a field7e08ad5f9976
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.instIsDiscreteValuationRing |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Inverse |
| note | — | `instance : IsDiscreteValuationRing k⟦X⟧` in `PowerSeries/Inverse.lean`, with `maximalIdeal_eq_span_X` giving X as the uniformizer. |
| status | — | formalized |
modifiedDivision as product with inversec1fb6d2d7a7c
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.inv |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Inverse |
| note | — | Division reduces to `B * A⁻¹` via `PowerSeries.inv`; over a field a full `Div` instance follows from the `Field` structure. |
| status | — | partial |
modifiedCoefficient extraction operator notation7700cba1f4f2
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.coeff |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Basic |
| note | — | Same as the earlier coefficient definition; notation like `[X^n]` is not scoped in Mathlib but `coeff n φ` plays the role. |
| status | — | formalized |
modifiedComposition of formal power series96456f62a014
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.subst |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Substitution |
| note | — | `PowerSeries.subst a f` (and `MvPowerSeries.subst`) formalize substitution/composition when `HasSubst a` holds. |
| status | — | formalized |
modifiedComposition validity conditiondf894633ebc8
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.HasSubst |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Substitution |
| note | — | `HasSubst a ↔ IsNilpotent (constantCoeff a)`; `subst` is only mathematically valid under this hypothesis. |
| status | — | formalized |
modifiedFaà di Bruno's formula49bed223bb6a
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | FormalMultilinearSeries.taylorComp |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno |
| note | — | Faà di Bruno is formalized only for iterated derivatives / Taylor composition in analysis, not for `PowerSeries.subst` coefficients. |
| status | — | partial |
modifiedLogarithmic series composition example93f52a24c69c
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.log |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Log |
| note | — | `PowerSeries.log` exists over ℚ-algebras; the article's specific composition example is not stated as a lemma. |
| status | — | partial |
modifiedExistence of composition inversee7dffe0c7d9b
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No general compositional-inverse existence theorem for `PowerSeries.subst` is present in Mathlib. |
| status | — | not_formalized |
modifiedFormal derivativeb51e149a1020
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.derivative |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Derivative |
| note | — | `PowerSeries.derivative R : Derivation R R⟦X⟧ R⟦X⟧` (notation `d⁄dX`). |
| status | — | formalized |
modifiedR-linearity of formal derivative2154fe26664d
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.derivative |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Derivative |
| note | — | Packaged as a `Derivation`, whose bundled type carries the `R`-linearity axioms `map_add'` and `map_smul'`. |
| status | — | formalized |
modifiedProduct rule497cf09ebad8
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.derivativeFun_mul |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Derivative |
| note | — | Labelled 'Leibniz rule for formal power series' in the file; built into the `Derivation` bundle. |
| status | — | formalized |
modifiedChain rulec5dd38936218
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.derivative_subst |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Derivative |
| note | — | `d⁄dX (f.subst g) = (d⁄dX f).subst g * d⁄dX g` under `HasSubst g`. |
| status | — | formalized |
modifiedFormal antiderivative4488be2940a4
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `PowerSeries.antiderivative` / formal integral operator exists in Mathlib. |
| status | — | not_formalized |
modifiedR-linearity of formal antiderivativecccac219c13b
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Depends on the missing formal antiderivative. |
| status | — | not_formalized |
modifiedAntiderivative is right inverse of derivative5442b5ef3bac
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Depends on the missing formal antiderivative. |
| status | — | not_formalized |
modifiedFormal power series ring contains polynomial ringf3499358128f
| Field | From #1232 | To #2793 |
|---|
| label | Polynomials as subring | Formal power series ring contains polynomial ring |
| mathlib.decl | — | Polynomial.coeToPowerSeries.algHom |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Basic |
| note | — | Relabeled: original 'Polynomials as subring' captured only part of the statement, which also asserts algebra structure. |
| provenance | ai-agent1 | ai-moderated |
| status | — | formalized |
modifiedJacobson radicalf281dbbdd218
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No lemma computing `Ring.jacobson R⟦X⟧` (or its containment) is present in the PowerSeries files. |
| status | — | not_formalized |
modifiedMaximal ideals characterization88a0c95faae7
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.maximalIdeal_eq_span_X |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Inverse |
| note | — | The unique maximal ideal of `k⟦X⟧` (k a field) is `(X)`; the correspondence with maximal ideals of general `R` is not stated. |
| status | — | partial |
modifiedAlgebraic properties inherited (local, Noetherian, etc.)2ccac1137e8b
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.instIsNoetherianRing |
| mathlib.match_kind | — | invocation |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Ideal |
| note | — | `IsNoetherianRing R⟦X⟧` for Noetherian R (`PowerSeries.Ideal`); `IsLocalRing` inheritance is in `MvPowerSeries.Inverse`. |
| status | — | formalized |
modifiedCompleteness of formal power series metricb956cf22730c
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.WithPiTopology.instCompleteSpace |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.PiTopology |
| note | — | Completeness is proved for the pi-uniform structure; there is no metric-space version because no metric is defined. |
| status | — | partial |
modifiedCompactness iff R finitee0c1884e20f8
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `CompactSpace (PowerSeries R) ↔ Finite R` lemma found in the PowerSeries files. |
| status | — | not_formalized |
modifiedWeierstrass preparation theoremaef63a3f5f1c
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.exists_isWeierstrassFactorization |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.WeierstrassPreparation |
| note | — | For a complete local ring, any power series whose image in the residue field is nonzero factors as (distinguished polynomial)·(unit). |
| status | — | formalized |
modifiedInterpreting formal power series as functions78e06f82fda8
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.aeval |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Evaluation |
| note | — | `PowerSeries.aeval ha : R⟦X⟧ →ₐ[R] S` evaluates a power series at a topologically nilpotent element. |
| status | — | formalized |
modifiedExplicit multiplicative inverse formula8bba482a4766
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.coeff_invOfUnit |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Inverse |
| note | — | Recursive coefficient formula for `invOfUnit`. |
| status | — | formalized |
modifiedFormal Laurent series0c12ddfa97ad
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | LaurentSeries |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.LaurentSeries |
| note | — | `LaurentSeries R := HahnSeries ℤ R`, notation `R⸨X⸩`. |
| status | — | formalized |
modifiedOrder of a formal Laurent seriesabafe7312d4a
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | HahnSeries.order |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.RingTheory.HahnSeries.Basic |
| note | — | `HahnSeries.order` / `orderTop` specializes to `LaurentSeries` since it is `HahnSeries ℤ`. |
| status | — | formalized |
modifiedLaurent series of order -38a098d77cffd
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Illustrative example, not a named lemma. |
| status | — | not_formalized |
modifiedMultiplication of formal Laurent series156200864476
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | HahnSeries.instMul |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.RingTheory.HahnSeries.Multiplication |
| note | — | Multiplication is inherited from the `HahnSeries` (semi)ring structure. |
| status | — | formalized |
modifiedRing of formal Laurent series as localization886ad66ca522
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | LaurentSeries.of_powerSeries_localization |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.LaurentSeries |
| note | — | `IsLocalization (Submonoid.powers X) R⸨X⸩` witnesses `R⸨X⸩ = R⟦X⟧[X⁻¹]`. |
| status | — | formalized |
modifiedFormal derivative of Laurent series8dac3822f501
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | LaurentSeries.derivative |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.LaurentSeries |
| note | — | `LaurentSeries.derivative = hasseDeriv 1`; a general `hasseDeriv k` operator is also defined. |
| status | — | formalized |
modifiedFormal residue7acd7dccf3f5
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `LaurentSeries.residue` (coefficient at X⁻¹ as a K-derivation) in Mathlib. |
| status | — | not_formalized |
modifiedResidue map exact sequencece9f6d255f13
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Depends on the missing formal residue. |
| status | — | not_formalized |
modifiedRules of calculus for formal residue41d264aa75cc
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Depends on the missing formal residue. |
| status | — | not_formalized |
modifiedLagrange inversion formula7e768e3434b8
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Lagrange inversion formula for formal power series in Mathlib. |
| status | — | not_formalized |
modifiedGeneralization of Lagrange inversiona81efebea88d
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | The basic Lagrange inversion theorem is not yet in Mathlib. |
| status | — | not_formalized |
modifiedFormal power series in several variables0ed52806cf28
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | MvPowerSeries |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.MvPowerSeries.Basic |
| note | — | `MvPowerSeries σ R := (σ →₀ ℕ) → R`. |
| status | — | formalized |
modifiedTopology on series in several variables3b7507cd5a1d
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | MvPowerSeries.WithPiTopology |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.MvPowerSeries.PiTopology |
| note | — | Product/pi topology on `MvPowerSeries σ R`. |
| status | — | formalized |
modifiedInvertibility in several variables48d8fc0bd75b
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | MvPowerSeries.isUnit_iff_constantCoeff |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.MvPowerSeries.Inverse |
| note | — | `IsUnit φ ↔ IsUnit (constantCoeff φ)` for `MvPowerSeries σ R`. |
| status | — | formalized |
modifiedComposition in several variables0286af3aa078
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | MvPowerSeries.subst |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.MvPowerSeries.Substitution |
| note | — | `MvPowerSeries.subst a f` under `MvPowerSeries.HasSubst a`. |
| status | — | formalized |
modifiedPartial derivative operatorsa9c0c5129306
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `MvPowerSeries.pderiv` defined in Mathlib (unlike `MvPolynomial.pderiv`). |
| status | — | not_formalized |
modifiedUniversal property (several variables)2ba76c51ae53
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | MvPowerSeries.aeval_unique |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.MvPowerSeries.Evaluation |
| note | — | A continuous R-algebra hom `MvPowerSeries σ R →ₐ[R] S` is determined by its values on X_s. |
| status | — | formalized |
modifiedNon-commuting variables / Magnus ringc24f809f388c
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No Magnus ring / noncommutative-variable formal power series construction in Mathlib. |
| status | — | not_formalized |
modifiedFormal power series over a semiring9f51278e403b
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | MvPowerSeries |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.MvPowerSeries.Basic |
| note | — | The Mathlib definition is already given for `[Semiring R]` (and `PowerSeries` inherits). |
| status | — | formalized |
modifiedSupport and characteristic series4889478db58e
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No `PowerSeries.support` or characteristic-series construction; `HahnSeries.support` exists but that is a different object. |
| status | — | not_formalized |
modifiedSum, Cauchy product, Hadamard product on a semiringeaf364375a08
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | PowerSeries.coeff_mul |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.RingTheory.PowerSeries.Basic |
| note | — | Addition and Cauchy product are provided by the (semi)ring instance; no Hadamard-product operator is defined for `PowerSeries`. |
| status | — | partial |
modifiedFormal power series on an ordered abelian group4064f0e676e1
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | HahnSeries |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.HahnSeries.Basic |
| note | — | `HahnSeries Γ R` for a partially-ordered Γ with well-founded (isPWO) support. |
| status | — | formalized |
modifiedHahn series field properties293fe538bc6b
| Field | From #1232 | To #2793 |
|---|
| mathlib.decl | — | HahnSeries.instField |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.RingTheory.HahnSeries.Summable |
| note | — | `HahnSeries Γ R` is a field when Γ is a linearly ordered abelian group and R is a field. |
| status | — | formalized |
addedUniqueness of multiplicative inversef8a2e3bfed78
addedCauchy product finiteness of each coefficientf2e39f18e746
addedEmbedding of R into R[[X]] and the indeterminate Xe568d9fe41e1
addedEquivalence of product/I-adic/metric topologies61ac90b3a80a
addedRecursive formula for coefficients of the n-th power84e65b36bd57
addedExponent rules for complex powers4a36928c2cdf
addedRecursive formula for coefficients of the inverse series443bbce2906b
addedCoefficient of composition via truncated polynomials1dc8270786d7
addedRecursive computation of composition inverse coefficients9ebbba45aedb
addedTaylor-series representation via formal derivativesbddd01401dc4
addedField of fractions of K[[X]] equals K((X))8a8f80abeb53
addedOrder/derivative relation ord(f') = ord(f) - 1b61e777970e7
addedFormal residue is a K-derivation7e1803ee1f34
addedLagrange inversion n=1 special caseebb68a0f4d1c