feat: port/RingTheory.Localization.Basic (#2741)

leanprover-community · Mar 9, 2023 · 0e402e9 · 0e402e9
1 parent 4613757
commit 0e402e9
Show file tree

Hide file tree

Showing 3 changed files with 1,418 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1163,6 +1163,7 @@ import Mathlib.RingTheory.Fintype
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Localization.Basic
 import Mathlib.RingTheory.NonZeroDivisors
 import Mathlib.RingTheory.OreLocalization.Basic
 import Mathlib.RingTheory.OreLocalization.OreSet

diff --git a/Mathlib/Algebra/Ring/Equiv.lean b/Mathlib/Algebra/Ring/Equiv.lean
@@ -259,6 +259,11 @@ theorem symm_symm (e : R ≃+* S) : e.symm.symm = e :=
   ext fun _ => rfl
 #align ring_equiv.symm_symm RingEquiv.symm_symm
 
+--Porting note: new theorem
+@[simp]
+theorem symm_refl : (RingEquiv.refl R).symm = RingEquiv.refl R :=
+  rfl
+
 @[simp]
 theorem coe_toEquiv_symm (e : R ≃+* S) : (e.symm : S ≃ R) = (e : R ≃ S).symm :=
   rfl
@@ -509,7 +514,7 @@ in higher generality -/
 
 
 @[simp]
-theorem coe_ringHom_refl : (RingEquiv.refl R : R →* R) = RingHom.id R :=
+theorem coe_ringHom_refl : (RingEquiv.refl R : R →+* R) = RingHom.id R :=
   rfl
 #align ring_equiv.coe_ring_hom_refl RingEquiv.coe_ringHom_refl