From 8226bfd4cca1e656295fe2c5275b1e745e4b7cfd Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Tue, 21 May 2024 13:27:07 +0200 Subject: [PATCH] Fix after merge --- Mathlib/RingTheory/Ideal/Maps.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean index eeb0cf36aa5ff..d06eee501fb11 100644 --- a/Mathlib/RingTheory/Ideal/Maps.lean +++ b/Mathlib/RingTheory/Ideal/Maps.lean @@ -959,10 +959,10 @@ theorem associatesEquivIsPrincipal_mem_nonZeroDivisors {x : R} : /-- A version of `Ideal.associatesEquivIsPrincipal` for non-zero-divisor generators. -/ def associatesNonZeroDivisorsEquivIsPrincipal : Associates R⁰ ≃ {I : (Ideal R)⁰ // IsPrincipal (I : Ideal R)} := - calc Associates R⁰ ≃ (Associates R)⁰ := (AssociatesNonZeroDivisorsMulEquiv R).toEquiv + calc Associates R⁰ ≃ (Associates R)⁰ := associatesNonZeroDivisorsEquiv.toEquiv.symm _ ≃ {I : {I : Ideal R // IsPrincipal I} // I.1 ∈ (Ideal R)⁰} := Equiv.subtypeEquiv (Ideal.associatesEquivIsPrincipal R) - (fun x ↦ by rw [← Associates.quot_out x, Associates_mk_mem_nonZeroDivisors_iff, + (fun x ↦ by rw [← Associates.quot_out x, mk_mem_nonZeroDivisors_associates, Ideal.associatesEquivIsPrincipal_mem_nonZeroDivisors]) _ ≃ {I : Ideal R // IsPrincipal I ∧ I ∈ (Ideal R)⁰} := Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ IsPrincipal I) (fun I ↦ I ∈ (Ideal R)⁰)