finprod_ne_zero — Mathlib

English

The multiplicity of v in the finprod ∏ v^(val_v(I)) equals the multiplicity of v in I's factorization.

Русский

Число v в произведении равняется числу v во факторизации I.

LaTeX

$$$(\text{Associates.mk } v.asIdeal).count (\prod^{\!\!\!} v : HeightOneSpectrum R, v.maxPowDividing I).factors = (\text{Associates.mk } v.asIdeal).count (\text{Associates.mk } I).factors$$$

Lean4

theorem finprod_ne_zero (I : Ideal R) : Associates.mk (∏ᶠ v : HeightOneSpectrum R, v.maxPowDividing I) ≠ 0 := by
  classical
  rw [Associates.mk_ne_zero, finprod_def]
  split_ifs
  · rw [Finset.prod_ne_zero_iff]
    intro v _
    apply pow_ne_zero _ v.ne_bot
  · exact one_ne_zero

Похожие утверждения