English
The equality of the fractional-product form with I holds, matching the nonzero ideal I.
Русский
Равенство дробной продукции с I сохраняется.
LaTeX
$$$(\prod^{\!\!\!} v : HeightOneSpectrum R, (v.asIdeal : FractionalIdeal R^0 K) ^((\Associates.mk v.asIdeal).count (Associates.mk I).factors : \mathbb{Z})).cast = FractionalIdeal.coeIdeal I$$$
Lean4
/-- The ideal `I` equals the finprod `∏_v v^(val_v(I))`, when both sides are regarded as fractional
ideals of `R`. -/
theorem finprod_heightOneSpectrum_factorization_coe {I : Ideal R} (hI : I ≠ 0) :
(∏ᶠ v : HeightOneSpectrum R,
(v.asIdeal : FractionalIdeal R⁰ K) ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ)) =
I :=
by
conv_rhs => rw [← Ideal.finprod_heightOneSpectrum_factorization hI]
rw [FractionalIdeal.coeIdeal_finprod R⁰ K (le_refl _)]
simp_rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FractionalIdeal.coeIdeal_pow, zpow_natCast]
