maxPowDividing_eq_pow_multiset_count

English

Over a Dedekind domain A, for a nonzero ideal I, maxPowDividing over heights equals v.asIdeal raised to the count of v in the normalized factorization of I.

Русский

Для ненулевого идеала I в Дедекенд домене A максимальная степень деления узла над I равна AsIdeal возведённой в счётчик v в нормализованном разложении I.

LaTeX

$$$\maxPowDividing v I = v.asIdeal^{\mathrm{count}_{v}(\text{normalizedFactors } I)}$$$

Lean4

theorem maxPowDividing_eq_pow_multiset_count [DecidableEq (Ideal R)] {I : Ideal R} (hI : I ≠ 0) :
    maxPowDividing v I = v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I) := by
  classical
    rw [maxPowDividing, factors_mk _ hI, count_some (irreducible_mk.mpr v.irreducible), ←
    Multiset.count_map_eq_count' _ _ Subtype.val_injective, map_subtype_coe_factors', factors_eq_normalizedFactors, ←
    Multiset.count_map_eq_count' _ _ (mk_injective (M := Ideal R))]

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