From 5a547aa92cbde6097c32d0e76ea8e51cf09afc62 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Fri, 18 Mar 2022 14:52:26 +0000 Subject: [PATCH] fix(ring_theory/power_series/basic): remove duplicate instance (#12744) --- src/ring_theory/power_series/basic.lean | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/ring_theory/power_series/basic.lean b/src/ring_theory/power_series/basic.lean index d65c1c43286be..fcbfa66234d62 100644 --- a/src/ring_theory/power_series/basic.lean +++ b/src/ring_theory/power_series/basic.lean @@ -648,7 +648,7 @@ section comm_ring variable [comm_ring R] /-- Multivariate formal power series over a local ring form a local ring. -/ -instance is_local_ring [local_ring R] : local_ring (mv_power_series σ R) := +instance [local_ring R] : local_ring (mv_power_series σ R) := { is_local := by { intro φ, rcases local_ring.is_local (constant_coeff σ R φ) with ⟨u,h⟩|⟨u,h⟩; [left, right]; { refine is_unit_of_mul_eq_one _ _ (mul_inv_of_unit _ u _), @@ -677,11 +677,6 @@ instance map.is_local_ring_hom : is_local_ring_hom (map σ f) := exact is_unit_of_mul_eq_one φ (inv_of_unit φ c) (mul_inv_of_unit φ c hc.symm) end⟩ -variables [local_ring R] [local_ring S] - -instance : local_ring (mv_power_series σ R) := -{ is_local := local_ring.is_local } - end local_ring section field