From dc4b2a8d2fadeb2a12efe631c21f68b07a579e53 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 21 Mar 2024 13:04:19 +0000 Subject: [PATCH] chore(HahnSeries): fix `Fintype`/`Finite` (#11531) --- Mathlib/RingTheory/HahnSeries/PowerSeries.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/HahnSeries/PowerSeries.lean b/Mathlib/RingTheory/HahnSeries/PowerSeries.lean index 6fe3429cc89968..c9eb3b9ff110d7 100644 --- a/Mathlib/RingTheory/HahnSeries/PowerSeries.lean +++ b/Mathlib/RingTheory/HahnSeries/PowerSeries.lean @@ -154,13 +154,13 @@ theorem ofPowerSeries_X_pow {R} [CommSemiring R] (n : ℕ) : #align hahn_series.of_power_series_X_pow HahnSeries.ofPowerSeries_X_pow -- Lemmas about converting hahn_series over fintype to and from mv_power_series -/-- The ring `HahnSeries (σ →₀ ℕ) R` is isomorphic to `MvPowerSeries σ R` for a `Fintype` `σ`. +/-- The ring `HahnSeries (σ →₀ ℕ) R` is isomorphic to `MvPowerSeries σ R` for a `Finite` `σ`. We take the index set of the hahn series to be `Finsupp` rather than `pi`, -even though we assume `Fintype σ` as this is more natural for alignment with `MvPowerSeries`. +even though we assume `Finite σ` as this is more natural for alignment with `MvPowerSeries`. After importing `Algebra.Order.Pi` the ring `HahnSeries (σ → ℕ) R` could be constructed instead. -/ @[simps] -def toMvPowerSeries {σ : Type*} [Fintype σ] : HahnSeries (σ →₀ ℕ) R ≃+* MvPowerSeries σ R where +def toMvPowerSeries {σ : Type*} [Finite σ] : HahnSeries (σ →₀ ℕ) R ≃+* MvPowerSeries σ R where toFun f := f.coeff invFun f := ⟨(f : (σ →₀ ℕ) → R), Finsupp.isPWO _⟩ left_inv f := by @@ -187,7 +187,7 @@ def toMvPowerSeries {σ : Type*} [Fintype σ] : HahnSeries (σ →₀ ℕ) R ≃ rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)] #align hahn_series.to_mv_power_series HahnSeries.toMvPowerSeries -variable {σ : Type*} [Fintype σ] +variable {σ : Type*} [Finite σ] theorem coeff_toMvPowerSeries {f : HahnSeries (σ →₀ ℕ) R} {n : σ →₀ ℕ} : MvPowerSeries.coeff R n (toMvPowerSeries f) = f.coeff n :=