English
The same height-one factorization holds when regarded as fractional ideals over R.
Русский
Та же факторизация над R в дробном виде.
LaTeX
$$$\text{finprod_heightOneSpectrum_factorization_coe} (I) :\; (\prod^{\!\!\!} v, (v.asIdeal : FractionalIdeal R^0 K) ^ (\mathrm{count}(v.asIdeal) \text{ в } \text{normalizedFactors } I)) = I$$$
Lean4
/-- The ideal `I` equals the finprod `∏_v v^(val_v(I))`. -/
theorem finprod_heightOneSpectrum_factorization {I : Ideal R} (hI : I ≠ 0) :
∏ᶠ v : HeightOneSpectrum R, v.maxPowDividing I = I :=
by
rw [← associated_iff_eq, ← Associates.mk_eq_mk_iff_associated]
classical
apply Associates.eq_of_eq_counts
· apply Associates.finprod_ne_zero I
· apply Associates.mk_ne_zero.mpr hI
intro v hv
obtain ⟨J, hJv⟩ := Associates.exists_rep v
rw [← hJv, Associates.irreducible_mk] at hv
rw [← hJv]
apply Ideal.finprod_count ⟨J, Ideal.isPrime_of_prime (irreducible_iff_prime.mp hv), Irreducible.ne_zero hv⟩ I hI
