English
If a multiset of normalized factors is uniquely equal to a single prime p, then r is associated to p^i for some i.
Русский
Если нормализованные факторы r состоят единственным вне единиц п, то r ассоциировано с p^i для некоторого i.
LaTeX
$$(∀ {p} (h : ∀ {m}, m ∈ normalizedFactors r → m = p)) ∧ (r ≠ 0) → ∃ i, Associated(p^i, r)$$
Lean4
theorem exists_associated_prime_pow_of_unique_normalized_factor {p r : α} (h : ∀ {m}, m ∈ normalizedFactors r → m = p)
(hr : r ≠ 0) : ∃ i : ℕ, Associated (p ^ i) r :=
by
use (normalizedFactors r).card
have := UniqueFactorizationMonoid.prod_normalizedFactors hr
rwa [Multiset.eq_replicate_of_mem fun b => h, Multiset.prod_replicate] at this
