case h
R : Type u_2
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.60520
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ x✝ ∈ associatedPrimes R M ↔ x✝ ∈ ∅
R : Type u_2
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.60520
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
⊢ associatedPrimes R M = ∅
ext
case h
R : Type u_2
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.60520
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ ¬x✝ ∈ associatedPrimes R M
case h
R : Type u_2
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.60520
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ x✝ ∈ associatedPrimes R M ↔ x✝ ∈ ∅
simp only [Set.mem_empty_iff_false, iff_false_iff]
no goals
case h
R : Type u_2
inst✝⁵ : CommRing R
I J : Ideal R
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
M' : Type ?u.60520
inst✝² : AddCommGroup M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ ¬x✝ ∈ associatedPrimes R M
apply not_isAssociatedPrime_of_subsingleton