R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    {x | ↑x.asIdeal ^ (-↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I)))) ≠ 1}
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    (mulSupport fun v =>
      ↑v.asIdeal ^ (-↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))))
rw [mulSupport]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    {x | ¬↑x.asIdeal ^ ↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I))) = 1}
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    {x | ↑x.asIdeal ^ (-↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I)))) ≠ 1}
simp_rw [zpow_neg, Ne.def, inv_eq_one]
no goals
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ Set.Finite
    {x | ¬↑x.asIdeal ^ ↑(Associates.count (Associates.mk x.asIdeal) (Associates.factors (Associates.mk I))) = 1}
exact finite_mulSupport_coe hI