English
Same as is_pow_of_dvd_count, restated with possibly different parameter arrangement.
Русский
То же самое, что и is_pow_of_dvd_count, повторено с другой расстановкой параметров.
LaTeX
$$$$\\text{Repeated: } a \\neq 0 \\land (\\forall p, \\mathrm{Irreducible}(p) \\Rightarrow k \\mid \\mathrm{count}(p,a.factors)) \\Rightarrow \\exists b:\\; a = b^k.$$$$
Lean4
theorem is_pow_of_dvd_count {a : Associates α} (ha : a ≠ 0) {k : ℕ}
(hk : ∀ p : Associates α, Irreducible p → k ∣ count p a.factors) : ∃ b : Associates α, a = b ^ k :=
by
nontriviality α
obtain ⟨a0, hz, rfl⟩ := exists_non_zero_rep ha
rw [factors_mk a0 hz] at hk
have hk' : ∀ p, p ∈ factors' a0 → k ∣ (factors' a0).count p :=
by
rintro p -
have pp : p = ⟨p.val, p.2⟩ := by simp only [Subtype.coe_eta]
rw [pp, ← count_some p.2]
exact hk p.val p.2
obtain ⟨u, hu⟩ := Multiset.exists_smul_of_dvd_count _ hk'
use FactorSet.prod (u : FactorSet α)
apply eq_of_factors_eq_factors
rw [pow_factors, prod_factors, factors_mk a0 hz, hu]
exact WithBot.coe_nsmul u k
