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
⊢ (∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))) =
    ↑(∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I)
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
⊢ (∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))) =
    ↑I
conv_rhs => rw [← Ideal.finprod_heightOneSpectrum_factorization I hI]
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
⊢ (∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))) =
    ∏ᶠ (a : HeightOneSpectrum R), ↑(maxPowDividing a I)
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
⊢ (∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))) =
    ↑(∏ᶠ (v : HeightOneSpectrum R), maxPowDividing v I)
rw [FractionalIdeal.coeIdeal_finprod R⁰ K (le_refl _)]
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
⊢ (∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk I)))) =
    ∏ᶠ (a : HeightOneSpectrum R), ↑(maxPowDividing a I)
simp_rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FractionalIdeal.coeIdeal_pow,
  zpow_ofNat]