[Merged by Bors] - chore(ring_theory/ideal/local_ring): generalize to semirings

src/logic/equiv/transfer_instance.lean

@@ -387,7 +387,7 @@ protected lemma local_ring {A B : Type*} [comm_ring A] [local_ring A] [comm_ring
   local_ring B :=
 begin
   haveI := e.symm.to_equiv.nontrivial,
-  refine @local_of_surjective A B _ _ _ _ e e.to_equiv.surjective,
+  refine @local_ring.of_surjective A B _ _ _ _ e e.to_equiv.surjective,
 end
 
 end ring_equiv

src/number_theory/padics/padic_integers.lean

@@ -537,7 +537,8 @@ section dvr
 /-! ### Discrete valuation ring -/
 
 instance : local_ring ℤ_[p] :=
-local_of_nonunits_ideal zero_ne_one $ by simp only [mem_nonunits]; exact λ x h y, norm_lt_one_add h
+local_ring.of_nonunits_ideal zero_ne_one $
+  by simp only [mem_nonunits]; exact λ x h y, norm_lt_one_add h
 
 lemma p_nonnunit : (p : ℤ_[p]) ∈ nonunits ℤ_[p] :=
 have (p : ℝ)⁻¹ < 1, from inv_lt_one $ by exact_mod_cast hp_prime.1.one_lt,

src/ring_theory/discrete_valuation_ring.lean

@@ -126,7 +126,7 @@ begin
       rw irreducible_iff_uniformizer at hQ2,
       exact hQ2.symm } },
   { rintro ⟨RPID, Punique⟩,
-    haveI : local_ring R := local_of_unique_nonzero_prime R Punique,
+    haveI : local_ring R := local_ring.of_unique_nonzero_prime Punique,
     refine {not_a_field' := _},
     rcases Punique with ⟨P, ⟨hP1, hP2⟩, hP3⟩,
     have hPM : P ≤ maximal_ideal R := le_maximal_ideal (hP2.1),

src/ring_theory/graded_algebra/homogeneous_localization.lean

@@ -470,28 +470,30 @@ end, λ ⟨⟨_, b, eq1, eq2⟩, rfl⟩, begin
   exact ⟨⟨f.val, b.val, eq1, eq2⟩, rfl⟩
 end⟩
 
+instance : nontrivial (homogeneous_localization 𝒜 x) :=
+⟨⟨0, 1, λ r, by simpa [ext_iff_val, zero_val, one_val, zero_ne_one] using r⟩⟩
+
 instance : local_ring (homogeneous_localization 𝒜 x) :=
-{ exists_pair_ne := ⟨0, 1, λ r, by simpa [ext_iff_val, zero_val, one_val, zero_ne_one] using r⟩,
-  is_local := λ a, begin
-    simp only [← is_unit_iff_is_unit_val, sub_val, one_val],
-    induction a using quotient.induction_on',
-    simp only [homogeneous_localization.val_mk', ← subtype.val_eq_coe],
-    by_cases mem1 : a.num.1 ∈ x,
-    { right,
-      have : a.denom.1 - a.num.1 ∈ x.prime_compl := λ h, a.denom_not_mem
-        ((sub_add_cancel a.denom.val a.num.val) ▸ ideal.add_mem _ h mem1 : a.denom.1 ∈ x),
-      apply is_unit_of_mul_eq_one _ (localization.mk a.denom.1 ⟨a.denom.1 - a.num.1, this⟩),
-      simp only [sub_mul, localization.mk_mul, one_mul, localization.sub_mk, ← subtype.val_eq_coe,
-        submonoid.coe_mul],
-      convert localization.mk_self _,
-      simp only [← subtype.val_eq_coe, submonoid.coe_mul],
-      ring, },
-    { left,
-      change _ ∈ x.prime_compl at mem1,
-      apply is_unit_of_mul_eq_one _ (localization.mk a.denom.1 ⟨a.num.1, mem1⟩),
-      rw [localization.mk_mul],
-      convert localization.mk_self _,
-      simpa only [mul_comm], },
-end }
+local_ring.of_is_unit_or_is_unit_one_sub_self $ λ a, begin
+  simp only [← is_unit_iff_is_unit_val, sub_val, one_val],
+  induction a using quotient.induction_on',
+  simp only [homogeneous_localization.val_mk', ← subtype.val_eq_coe],
+  by_cases mem1 : a.num.1 ∈ x,
+  { right,
+    have : a.denom.1 - a.num.1 ∈ x.prime_compl := λ h, a.denom_not_mem
+      ((sub_add_cancel a.denom.val a.num.val) ▸ ideal.add_mem _ h mem1 : a.denom.1 ∈ x),
+    apply is_unit_of_mul_eq_one _ (localization.mk a.denom.1 ⟨a.denom.1 - a.num.1, this⟩),
+    simp only [sub_mul, localization.mk_mul, one_mul, localization.sub_mk, ← subtype.val_eq_coe,
+      submonoid.coe_mul],
+    convert localization.mk_self _,
+    simp only [← subtype.val_eq_coe, submonoid.coe_mul],
+    ring, },
+  { left,
+    change _ ∈ x.prime_compl at mem1,
+    apply is_unit_of_mul_eq_one _ (localization.mk a.denom.1 ⟨a.num.1, mem1⟩),
+    rw [localization.mk_mul],
+    convert localization.mk_self _,
+    simpa only [mul_comm], },
+end
 
 end homogeneous_localization