count_le_of_ideal_ge — Mathlib

English

If I ≤ J and I ≠ ⊥ in a Dedekind domain with decidable equality, then for any K, the count of K in the factorization of J is at most that in I.

Русский

Если I ≤ J и I ≠ ⊥, то для любого K число появления K в разложении J не превосходит числа появления в I.

LaTeX

$$count K (normalizedFactors J) ≤ count K (normalizedFactors I)$$

Lean4

theorem count_le_of_ideal_ge [DecidableEq (Ideal T)] {I J : Ideal T} (h : I ≤ J) (hI : I ≠ ⊥) (K : Ideal T) :
    count K (normalizedFactors J) ≤ count K (normalizedFactors I) :=
  le_iff_count.1 ((dvd_iff_normalizedFactors_le_normalizedFactors (ne_bot_of_le_ne_bot hI h) hI).1 (dvd_iff_le.2 h)) _

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