chore(PowerSeries): remove duplicate instances (#37289)

JovanGerb · JovanGerb · commit e960b84129b3 · 2026-03-27T22:04:02.000Z
Since `PowerSeries` is an abbrev for `MvPowerSeries`, all instances are inherited automatically. This PR removes the duplicate instances.

There is a bunch of material duplicated in `PowerSeries/Inverse.lean` which is already proved in `MvPowerSeries/Inverse.lean`. That may be removed in a future PR.
diff --git a/Mathlib/RingTheory/PowerSeries/Basic.lean b/Mathlib/RingTheory/PowerSeries/Basic.lean
@@ -64,74 +64,12 @@ open Finsupp (single)
 
 variable {R : Type*}
 
-section
-
 /--
 `R⟦X⟧` is notation for `PowerSeries R`,
 the semiring of formal power series in one variable over a semiring `R`.
 -/
 scoped notation:9000 R "⟦X⟧" => PowerSeries R
 
-instance [Inhabited R] : Inhabited R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance [Zero R] : Zero R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance [AddMonoid R] : AddMonoid R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance [AddGroup R] : AddGroup R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance [AddCommMonoid R] : AddCommMonoid R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance [AddCommGroup R] : AddCommGroup R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance [Semiring R] : Semiring R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance [CommSemiring R] : CommSemiring R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance [Ring R] : Ring R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance [CommRing R] : CommRing R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance [Nontrivial R] : Nontrivial R⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-set_option backward.isDefEq.respectTransparency false in
-instance {A} [Semiring R] [AddCommMonoid A] [Module R A] : Module R A⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-instance {A S} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R A] [Module S A] [SMul R S]
-    [IsScalarTower R S A] : IsScalarTower R S A⟦X⟧ :=
-  Pi.isScalarTower
-
-set_option backward.isDefEq.respectTransparency false in
-instance {A} [Semiring A] [CommSemiring R] [Algebra R A] : Algebra R A⟦X⟧ := by
-  dsimp only [PowerSeries]
-  infer_instance
-
-end
-
 section Semiring
 
 variable [Semiring R]
@@ -229,7 +167,6 @@ theorem coeff_zero_eq_constantCoeff : ⇑(coeff (R := R) 0) = constantCoeff := b
 theorem coeff_zero_eq_constantCoeff_apply (φ : R⟦X⟧) : coeff 0 φ = constantCoeff φ := by
   rw [coeff_zero_eq_constantCoeff]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem monomial_zero_eq_C : ⇑(monomial (R := R) 0) = C := by
   -- This used to be `rw`, but we need `rw; rfl` after https://github.com/leanprover/lean4/pull/2644
@@ -268,7 +205,6 @@ theorem X_eq : (X : R⟦X⟧) = monomial 1 1 :=
 theorem coeff_X (n : ℕ) : coeff n (X : R⟦X⟧) = if n = 1 then 1 else 0 := by
   rw [X_eq, coeff_monomial]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem coeff_zero_X : coeff 0 (X : R⟦X⟧) = 0 := by
   rw [coeff, Finsupp.single_zero, X, MvPowerSeries.coeff_zero_X]
@@ -326,14 +262,12 @@ theorem smul_eq_C_mul (f : R⟦X⟧) (a : R) : a • f = C a * f := by
   ext
   simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem coeff_succ_mul_X (n : ℕ) (φ : R⟦X⟧) : coeff (n + 1) (φ * X) = coeff n φ := by
   simp only [coeff, Finsupp.single_add]
   convert φ.coeff_add_mul_monomial (single () n) (single () 1) _
   rw [mul_one]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem coeff_succ_X_mul (n : ℕ) (φ : R⟦X⟧) : coeff (n + 1) (X * φ) = coeff n φ := by
   simp only [coeff, Finsupp.single_add, add_comm n 1]
@@ -592,7 +526,6 @@ variable [CommSemiring R]
 
 open Finset Nat
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The ring homomorphism taking a power series `f(X)` to `f(aX)`. -/
 noncomputable def rescale (a : R) : R⟦X⟧ →+* R⟦X⟧ where
   toFun f := PowerSeries.mk fun n => a ^ n * PowerSeries.coeff n f
@@ -670,7 +603,6 @@ open Finset.HasAntidiagonal Finset
 
 variable {R : Type*} [CommSemiring R] {ι : Type*}
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Coefficients of a product of power series -/
 theorem coeff_prod [DecidableEq ι] (f : ι → PowerSeries R) (d : ℕ) (s : Finset ι) :
     coeff d (∏ j ∈ s, f j) = ∑ l ∈ finsuppAntidiag s d, ∏ i ∈ s, coeff (l i) (f i) := by
@@ -710,7 +642,6 @@ lemma coeff_one_mul (φ ψ : R⟦X⟧) : coeff 1 (φ * ψ) =
     mul_comm, add_comm]
   simp
 
-set_option backward.isDefEq.respectTransparency false in
 /-- First coefficient of the `n`-th power of a power series. -/
 lemma coeff_one_pow (n : ℕ) (φ : R⟦X⟧) :
     coeff 1 (φ ^ n) = n * coeff 1 φ * (constantCoeff φ) ^ (n - 1) := by
@@ -747,7 +678,6 @@ section CommRing
 
 variable {A : Type*} [CommRing A]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem not_isField : ¬IsField A⟦X⟧ := by
   by_cases hA : Subsingleton A
   · exact not_isField_of_subsingleton _
@@ -767,7 +697,6 @@ theorem rescale_X (a : A) : rescale a X = C a * X := by
   simp only [coeff_rescale, coeff_C_mul, coeff_X]
   split_ifs with h <;> simp [h]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem rescale_neg_one_X : rescale (-1 : A) X = -X := by
   rw [rescale_X, map_neg, map_one, neg_one_mul]
 
@@ -791,7 +720,6 @@ theorem C_eq_algebraMap {r : R} : C r = (algebraMap R R⟦X⟧) r :=
 theorem algebraMap_apply {r : R} : algebraMap R A⟦X⟧ r = C (algebraMap R A r) :=
   MvPowerSeries.algebraMap_apply
 
-set_option backward.isDefEq.respectTransparency false in
 instance [Nontrivial R] : Nontrivial (Subalgebra R R⟦X⟧) :=
   { (inferInstance : Nontrivial <| Subalgebra R <| MvPowerSeries Unit R) with }
 
@@ -914,7 +842,6 @@ theorem coeToPowerSeries.ringHom_apply : coeToPowerSeries.ringHom φ = φ :=
 theorem coe_pow (n : ℕ) : ((φ ^ n : R[X]) : PowerSeries R) = (φ : PowerSeries R) ^ n :=
   coeToPowerSeries.ringHom.map_pow _ _
 
-set_option backward.isDefEq.respectTransparency false in
 theorem eval₂_C_X_eq_coe : φ.eval₂ PowerSeries.C PowerSeries.X = ↑φ := by
   nth_rw 2 [← eval₂_C_X (p := φ)]
   rw [← coeToPowerSeries.ringHom_apply, eval₂_eq_sum_range, eval₂_eq_sum_range, map_sum]
@@ -929,7 +856,6 @@ section CommSemiring
 
 variable {R : Type*} [CommSemiring R] (φ ψ : R[X])
 
-set_option backward.isDefEq.respectTransparency false in
 theorem _root_.MvPolynomial.toMvPowerSeries_pUnitAlgEquiv {f : MvPolynomial PUnit R} :
     (f.toMvPowerSeries : PowerSeries R) = (f.pUnitAlgEquiv R).toPowerSeries := by
   induction f using MvPolynomial.induction_on' with
diff --git a/Mathlib/RingTheory/PowerSeries/Inverse.lean b/Mathlib/RingTheory/PowerSeries/Inverse.lean
@@ -52,7 +52,6 @@ variable [Ring R]
 protected def inv.aux : R → R⟦X⟧ → R⟦X⟧ :=
   MvPowerSeries.inv.aux
 
-set_option backward.isDefEq.respectTransparency false in
 theorem coeff_inv_aux (n : ℕ) (a : R) (φ : R⟦X⟧) :
     coeff n (inv.aux a φ) =
       if n = 0 then a
@@ -129,11 +128,9 @@ section Field
 variable {k : Type*} [Field k]
 
 /-- The inverse 1/f of a power series f defined over a field -/
-protected def inv : k⟦X⟧ → k⟦X⟧ :=
+protected abbrev inv : k⟦X⟧ → k⟦X⟧ :=
   MvPowerSeries.inv
 
-instance : Inv k⟦X⟧ := ⟨PowerSeries.inv⟩
-
 theorem inv_eq_inv_aux (φ : k⟦X⟧) : φ⁻¹ = inv.aux (constantCoeff φ)⁻¹ φ :=
   rfl
 
@@ -189,9 +186,6 @@ theorem inv_eq_iff_mul_eq_one {φ ψ : k⟦X⟧} (h : constantCoeff ψ ≠ 0) :
 protected theorem mul_inv_rev (φ ψ : k⟦X⟧) : (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹ :=
   MvPowerSeries.mul_inv_rev _ _
 
-instance : InvOneClass k⟦X⟧ :=
-  { (inferInstance : InvOneClass <| MvPowerSeries Unit k) with }
-
 @[simp]
 theorem C_inv (r : k) : (C r)⁻¹ = C r⁻¹ :=
   MvPowerSeries.C_inv _
@@ -222,7 +216,6 @@ theorem Inv_divided_by_X_pow_order_rightInv {f : k⟦X⟧} (hf : f ≠ 0) :
     divXPowOrder f * Inv_divided_by_X_pow_order hf = 1 :=
   mul_invOfUnit (divXPowOrder f) (firstUnitCoeff hf) rfl
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Inv_divided_by_X_pow_order_leftInv {f : k⟦X⟧} (hf : f ≠ 0) :
     Inv_divided_by_X_pow_order hf * divXPowOrder f = 1 := by
@@ -253,7 +246,6 @@ theorem Unit_of_divided_by_X_pow_order_nonzero {f : k⟦X⟧} (hf : f ≠ 0) :
 theorem Unit_of_divided_by_X_pow_order_zero : Unit_of_divided_by_X_pow_order (0 : k⟦X⟧) = 1 := by
   simp only [Unit_of_divided_by_X_pow_order, dif_pos]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem eq_divided_by_X_pow_order_Iff_Unit {f : k⟦X⟧} (hf : f ≠ 0) :
     f = divXPowOrder f ↔ IsUnit f :=
   ⟨fun h ↦ by rw [h]; exact isUnit_divided_by_X_pow_order hf, fun h ↦ by
@@ -274,11 +266,6 @@ theorem map.isLocalHom : IsLocalHom (map f) :=
 
 variable [IsLocalRing R]
 
-set_option backward.isDefEq.respectTransparency false in
-instance : IsLocalRing R⟦X⟧ :=
-  { (inferInstance : IsLocalRing <| MvPowerSeries Unit R) with }
-
-
 end IsLocalRing
 
 section IsDiscreteValuationRing
@@ -297,19 +284,14 @@ theorem hasUnitMulPowIrreducibleFactorization :
         simp only [Unit_of_divided_by_X_pow_order_nonzero hf]
         exact X_pow_order_mul_divXPowOrder)⟩
 
-set_option backward.isDefEq.respectTransparency false in
 instance : UniqueFactorizationMonoid k⟦X⟧ :=
   hasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid
 
-set_option backward.isDefEq.respectTransparency false in
 instance : IsDiscreteValuationRing k⟦X⟧ :=
   ofHasUnitMulPowIrreducibleFactorization hasUnitMulPowIrreducibleFactorization
 
-set_option backward.isDefEq.respectTransparency false in
-instance isNoetherianRing : IsNoetherianRing k⟦X⟧ :=
-  PrincipalIdealRing.isNoetherianRing
+example : IsNoetherianRing k⟦X⟧ := inferInstance
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The maximal ideal of `k⟦X⟧` is generated by `X`. -/
 theorem maximalIdeal_eq_span_X : IsLocalRing.maximalIdeal (k⟦X⟧) = Ideal.span {X} := by
   have hX : (Ideal.span {(X : k⟦X⟧)}).IsMaximal := by
@@ -331,7 +313,6 @@ theorem maximalIdeal_eq_span_X : IsLocalRing.maximalIdeal (k⟦X⟧) = Ideal.spa
       apply Ideal.eq_top_of_isUnit_mem I hfI0 (IsUnit.map C (Ne.isUnit hfX))
   rw [IsLocalRing.eq_maximalIdeal hX]
 
-set_option backward.isDefEq.respectTransparency false in
 set_option linter.style.whitespace false in -- manual alignment is not recognised
 instance : NormalizationMonoid k⟦X⟧ where
   normUnit f := (Unit_of_divided_by_X_pow_order f)⁻¹
@@ -348,17 +329,14 @@ instance : NormalizationMonoid k⟦X⟧ where
     rw [inv_inj, Units.ext_iff, ← hu, Unit_of_divided_by_X_pow_order_nonzero h₀.ne_zero]
     exact ((eq_divided_by_X_pow_order_Iff_Unit h₀.ne_zero).mpr h₀).symm
 
-set_option backward.isDefEq.respectTransparency false in
 theorem normUnit_X : normUnit (X : k⟦X⟧) = 1 := by
   simp [normUnit, ← Units.val_eq_one, Unit_of_divided_by_X_pow_order_nonzero]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem X_eq_normalizeX : (X : k⟦X⟧) = normalize X := by
   simp only [normalize_apply, normUnit_X, Units.val_one, mul_one]
 
 open UniqueFactorizationMonoid
 
-set_option backward.isDefEq.respectTransparency false in
 open scoped Classical in
 theorem normalized_count_X_eq_of_coe {P : k[X]} (hP : P ≠ 0) :
     Multiset.count PowerSeries.X (normalizedFactors (P : k⟦X⟧)) =
@@ -373,12 +351,10 @@ theorem normalized_count_X_eq_of_coe {P : k[X]} (hP : P ≠ 0) :
 
 open IsLocalRing
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ker_coeff_eq_max_ideal : RingHom.ker (constantCoeff (R := k)) = maximalIdeal _ :=
   Ideal.ext fun _ ↦ by
     rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The ring isomorphism between the residue field of the ring of power series valued in a field `K`
 and `K` itself. -/
 def residueFieldOfPowerSeries : ResidueField k⟦X⟧ ≃+* k :=
