English
Given I ≠ ⊥ and irreducible J, for any n the supremum equals J^multiplicity(J,I) when emultiplicity(I,J) ≤ n.
Русский
Если I ≠ ⊥ и J непр decomим, для любого n верхняя граница равна J^{multiplicity(J,I)} когда emultiplicity(I,J) ≤ n.
LaTeX
$$J^n ⊔ I = J^{multiplicity J I}$$
Lean4
theorem irreducible_pow_sup_of_ge (hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) (hn : emultiplicity J I ≤ n) :
J ^ n ⊔ I = J ^ multiplicity J I := by
classical
rw [irreducible_pow_sup hI hJ, min_eq_left]
· congr
rw [← Nat.cast_inj (R := ℕ∞), ← FiniteMultiplicity.emultiplicity_eq_multiplicity,
emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J]
rw [← emultiplicity_lt_top]
apply hn.trans_lt
simp
· rw [emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J] at hn
exact_mod_cast hn
