finite_mulSupport_inv — Mathlib

English

Taking negative exponents (inverse) preserves finiteness of mulSupport for nonzero I.

Русский

При отрицательных степенях поддержка остаётся конечной.

LaTeX

$$$\operatorname{mulSupport} \big( v.asIdeal^{-(\mathrm{count}(I) )} \big) \text{ finite}$$$

Lean4

/-- For every nonzero ideal `I` of `v`, there are finitely many maximal ideals `v` such that
`v^-(val_v(I))` is not the unit ideal. -/
theorem finite_mulSupport_inv {I : Ideal R} (hI : I ≠ 0) :
    (mulSupport fun v : HeightOneSpectrum R =>
        (v.asIdeal : FractionalIdeal R⁰ K) ^
          (-((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ))).Finite :=
  by
  rw [mulSupport]
  simp_rw [zpow_neg, Ne, inv_eq_one]
  exact finite_mulSupport_coe hI

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