English
There exists a maximal ideal Q such that P ⊔ Q = ⊤ and I equals P^k * Q, where k is the count of P in the normalized factorization of I.
Русский
Существует максимальный идеал Q такой, что P ⊔ Q = ⊤ и I = P^k * Q, где k есть число вхождений P в нормализованное разложение I.
LaTeX
$$∃ Q, P ⊔ Q = ⊤ ∧ I = P^count P (normalizedFactors I) * Q$$
Lean4
theorem eq_prime_pow_mul_coprime [DecidableEq (Ideal T)] {I : Ideal T} (hI : I ≠ ⊥) (P : Ideal T) [hpm : P.IsMaximal] :
∃ Q : Ideal T, P ⊔ Q = ⊤ ∧ I = P ^ (Multiset.count P (normalizedFactors I)) * Q :=
by
use (filter (¬P = ·) (normalizedFactors I)).prod
constructor
· refine P.sup_multiset_prod_eq_top (fun p hpi ↦ ?_)
have hp : Prime p := prime_of_normalized_factor p (filter_subset _ (normalizedFactors I) hpi)
exact hpm.coprime_of_ne ((isPrime_of_prime hp).isMaximal hp.ne_zero) (of_mem_filter hpi)
· nth_rw 1 [← prod_normalizedFactors_eq_self hI, ← filter_add_not (P = ·) (normalizedFactors I)]
rw [prod_add, pow_count]
