[Merged by Bors] - split power series in several files #10866

AntoineChambert-Loir · 2024-02-22T23:59:00Z

This PR split the files devoted to power series (especially RingTheory/PowerSeries/Basic) into several ones:

RingTheory/MvPowerSeries/Basic - initial definitions (multivariate)
RingTheory/MvPowerSeries/Trunc - truncation
RingTheory/MvPowerSeries/Inverse - stuff pertaining to inverses
RingTheory/PowerSeries/Basic - initial definitions (univariate)
RingTheory/PowerSeries/Trunc - truncation
RingTheory/PowerSeries/Inverse - stuff pertaining to inverses
RingTheory/PowerSeries/Order - stuff pertaining to order

it remains to adjust the other files (PowerSeries/Derivative and PowerSeries/WellKnown)

Mathlib/RingTheory/MvPowerSeries/Trunc.lean

…community/mathlib4 into ACL/splitPowerSeries

Mathlib/RingTheory/MvPowerSeries/Basic.lean

faenuccio · 2024-02-28T12:07:25Z

Mathlib/RingTheory/MvPowerSeries/Basic.lean

+
+end Map
+
+section Algebra


Why this interlude about Algebra is here? Shouldn't it be further below, together with the rest of the Algebra section?

Yes. But that section is about general algebras, and the next one is about the commutative case.

I see, I do not have a strong opinion here although I would slightly prefer the idea of "richer structures" being further down. But ignore this message if you prefer so.

In fact, not so much… the second Algebra section is about having polynomials into power series being an algHom. But I moved the algebra section after the commsemiring section, it is more logic.

Mathlib/RingTheory/MvPowerSeries/Basic.lean

Mathlib/RingTheory/MvPowerSeries/Inverse.lean

Mathlib/RingTheory/PowerSeries/Trunc.lean

Co-authored-by: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>

AntoineChambert-Loir · 2024-02-28T21:24:36Z

Mathlib/RingTheory/PowerSeries/Basic.lean

-theorem smul_inv (r : k) (φ : MvPowerSeries σ k) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹ := by
-  simp [smul_eq_C_mul, mul_comm]
-#align mv_power_series.smul_inv MvPowerSeries.smul_inv
-
-end Field
-
-end MvPowerSeries
-
-namespace MvPolynomial
-
-open Finsupp
-
-variable {σ : Type*} {R : Type*} [CommSemiring R] (φ ψ : MvPolynomial σ R)
-
-- Porting note: added so we can add the `@[coe]` attribute
-/-- The natural inclusion from multivariate polynomials into multivariate formal power series.-/
-@[coe]
-def toMvPowerSeries : MvPolynomial σ R → MvPowerSeries σ R :=
-  fun φ n => coeff n φ
-
-/-- The natural inclusion from multivariate polynomials into multivariate formal power series.-/
-instance coeToMvPowerSeries : Coe (MvPolynomial σ R) (MvPowerSeries σ R) :=
-  ⟨toMvPowerSeries⟩
-#align mv_polynomial.coe_to_mv_power_series MvPolynomial.coeToMvPowerSeries
-
-theorem coe_def : (φ : MvPowerSeries σ R) = fun n => coeff n φ :=
-  rfl
-#align mv_polynomial.coe_def MvPolynomial.coe_def
-
-@[simp, norm_cast]
-theorem coeff_coe (n : σ →₀ ℕ) : MvPowerSeries.coeff R n ↑φ = coeff n φ :=
-  rfl
-#align mv_polynomial.coeff_coe MvPolynomial.coeff_coe
-
-@[simp, norm_cast]
-theorem coe_monomial (n : σ →₀ ℕ) (a : R) :
-    (monomial n a : MvPowerSeries σ R) = MvPowerSeries.monomial R n a :=
-  MvPowerSeries.ext fun m => by
-    classical
-    rw [coeff_coe, coeff_monomial, MvPowerSeries.coeff_monomial]
-    split_ifs with h₁ h₂ <;> first |rfl|subst m; contradiction
-#align mv_polynomial.coe_monomial MvPolynomial.coe_monomial
-
-@[simp, norm_cast]
-theorem coe_zero : ((0 : MvPolynomial σ R) : MvPowerSeries σ R) = 0 :=
-  rfl
-#align mv_polynomial.coe_zero MvPolynomial.coe_zero
-
-@[simp, norm_cast]
-theorem coe_one : ((1 : MvPolynomial σ R) : MvPowerSeries σ R) = 1 :=
-    coe_monomial _ _
-#align mv_polynomial.coe_one MvPolynomial.coe_one
-
-@[simp, norm_cast]
-theorem coe_add : ((φ + ψ : MvPolynomial σ R) : MvPowerSeries σ R) = φ + ψ :=
-  rfl
-#align mv_polynomial.coe_add MvPolynomial.coe_add
-
-@[simp, norm_cast]
-theorem coe_mul : ((φ * ψ : MvPolynomial σ R) : MvPowerSeries σ R) = φ * ψ :=
-  MvPowerSeries.ext fun n => by
-    classical
-    simp only [coeff_coe, MvPowerSeries.coeff_mul, coeff_mul]
-#align mv_polynomial.coe_mul MvPolynomial.coe_mul
-
-@[simp, norm_cast]
-theorem coe_C (a : R) : ((C a : MvPolynomial σ R) : MvPowerSeries σ R) = MvPowerSeries.C σ R a :=
-  coe_monomial _ _
-set_option linter.uppercaseLean3 false in
-#align mv_polynomial.coe_C MvPolynomial.coe_C
-
-set_option linter.deprecated false in
-@[simp, norm_cast]
-theorem coe_bit0 :
-    ((bit0 φ : MvPolynomial σ R) : MvPowerSeries σ R) = bit0 (φ : MvPowerSeries σ R) :=
-  coe_add _ _
-#align mv_polynomial.coe_bit0 MvPolynomial.coe_bit0
-
-set_option linter.deprecated false in
-@[simp, norm_cast]
-theorem coe_bit1 :
-    ((bit1 φ : MvPolynomial σ R) : MvPowerSeries σ R) = bit1 (φ : MvPowerSeries σ R) := by
-  rw [bit1, bit1, coe_add, coe_one, coe_bit0]
-#align mv_polynomial.coe_bit1 MvPolynomial.coe_bit1
-
-@[simp, norm_cast]
-theorem coe_X (s : σ) : ((X s : MvPolynomial σ R) : MvPowerSeries σ R) = MvPowerSeries.X s :=
-  coe_monomial _ _
-set_option linter.uppercaseLean3 false in
-#align mv_polynomial.coe_X MvPolynomial.coe_X
-
-variable (σ R)
-
-theorem coe_injective : Function.Injective (Coe.coe : MvPolynomial σ R → MvPowerSeries σ R) :=
-    fun x y h => by
-  ext
-  simp_rw [← coeff_coe]
-  congr
-#align mv_polynomial.coe_injective MvPolynomial.coe_injective
+import Mathlib.RingTheory.MvPowerSeries.Basic


What do you mean?

…cstring.

…community/mathlib4 into ACL/splitPowerSeries

faenuccio · 2024-02-29T12:18:41Z

Thanks, LGTM.

riccardobrasca · 2024-02-29T12:19:44Z

This is surely better than the current situation, thanks!

bors merge

This PR split the files devoted to power series (especially RingTheory/PowerSeries/Basic) into several ones: * RingTheory/MvPowerSeries/Basic - initial definitions (multivariate) * RingTheory/MvPowerSeries/Trunc - truncation * RingTheory/MvPowerSeries/Inverse - stuff pertaining to inverses * RingTheory/PowerSeries/Basic - initial definitions (univariate) * RingTheory/PowerSeries/Trunc - truncation * RingTheory/PowerSeries/Inverse - stuff pertaining to inverses * RingTheory/PowerSeries/Order - stuff pertaining to order it remains to adjust the other files (PowerSeries/Derivative and PowerSeries/WellKnown) Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: faenuccio <filippo.nuccio@univ-st-etienne.fr>

mathlib-bors · 2024-02-29T13:07:16Z

Pull request successfully merged into master.

Build succeeded:

This PR split the files devoted to power series (especially RingTheory/PowerSeries/Basic) into several ones: * RingTheory/MvPowerSeries/Basic - initial definitions (multivariate) * RingTheory/MvPowerSeries/Trunc - truncation * RingTheory/MvPowerSeries/Inverse - stuff pertaining to inverses * RingTheory/PowerSeries/Basic - initial definitions (univariate) * RingTheory/PowerSeries/Trunc - truncation * RingTheory/PowerSeries/Inverse - stuff pertaining to inverses * RingTheory/PowerSeries/Order - stuff pertaining to order it remains to adjust the other files (PowerSeries/Derivative and PowerSeries/WellKnown) Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: faenuccio <filippo.nuccio@univ-st-etienne.fr>

split power series (some cleanup still needed)

b8c09e9

AntoineChambert-Loir added the WIP Work in progress label Feb 22, 2024

Antoine Chambert-Loir added 10 commits February 23, 2024 01:01

adjust headers

d632cb4

adjust Mathlib.lean

01eb9ad

try to adjust imports of PowerSeries/Derivative

a99bcf8

add import to Bernoulli

4b86801

adjust Archive/Wiedijk100Theorems/Partition

3ea748a

adjust import

10ffbd6

adjust import

f5d62dc

adjust import (should work this time)

b8e8f7c

adjust import

f686341

delete passages that were commented out and copied in other files

a3f8e1f

AntoineChambert-Loir added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Feb 23, 2024

Merge branch 'master' into ACL/splitPowerSeries

4558b56

jcommelin added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Feb 28, 2024

jcommelin reviewed Feb 28, 2024

View reviewed changes

Mathlib/RingTheory/MvPowerSeries/Trunc.lean Outdated Show resolved Hide resolved

jcommelin added awaiting-CI and removed auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. labels Feb 28, 2024

Antoine Chambert-Loir added 2 commits February 28, 2024 09:01

remove "-- import …"

375476c

Merge branch 'ACL/splitPowerSeries' of https://github.com/leanprover-…

833830b

…community/mathlib4 into ACL/splitPowerSeries

github-actions bot removed the awaiting-CI label Feb 28, 2024

riccardobrasca requested a review from faenuccio February 28, 2024 08:37