English
In a unique factorization monoid with zero, every divisor of a prime power p^n is itself a power of p; precisely, if a divides p^n then a = p^{count(a.factors)}.
Русский
В моноиде с уникализацией и нулём каждый делитель степенного простого p^n является степенью p; точнее, если a | p^n, то a = p^{count(a.factors)}.
LaTeX
$$$\\forall {p,a} \\ (hp : Irreducible\, p) \\, \\forall {n:\\mathbb{N}}\\ (h : a \\mid p^n) \\Rightarrow a = p^{p.count\\, a.factors}$$$
Lean4
/-- The only divisors of prime powers are prime powers. See `eq_pow_find_of_dvd_irreducible_pow`
for an explicit expression as a p-power (without using `count`). -/
theorem eq_pow_count_factors_of_dvd_pow {p a : Associates α} (hp : Irreducible p) {n : ℕ} (h : a ∣ p ^ n) :
a = p ^ p.count a.factors := by
nontriviality α
have hph := pow_ne_zero n hp.ne_zero
have ha := ne_zero_of_dvd_ne_zero hph h
apply eq_of_eq_counts ha (pow_ne_zero _ hp.ne_zero)
have eq_zero_of_ne : ∀ q : Associates α, Irreducible q → q ≠ p → _ = 0 := fun q hq h' =>
Nat.eq_zero_of_le_zero <| by
convert count_le_count_of_le hph hq h
symm
rw [count_pow hp.ne_zero hq, count_eq_zero_of_ne hq hp h', mul_zero]
intro q hq
rw [count_pow hp.ne_zero hq]
by_cases h : q = p
· rw [h, count_self hp, mul_one]
· rw [count_eq_zero_of_ne hq hp h, mul_zero, eq_zero_of_ne q hq h]
