English
If n is squarefree and p is a prime factor of n, then for any f ∈ finMulAntidiag d n there exists a unique i with p dividing f(i).
Русский
Если n квадратно-безкратно и p — простой делитель n, тогда для любой f ∈ finMulAntidiag d n существует единственный индекс i, для которого p делит f(i).
LaTeX
$$$\forall f\in\text{finMulAntidiag}(d,n),\exists! i, p\mid f(i)$ (при условии розрядности $n$ и квадратно-безкратности)$$
Lean4
theorem finMulAntidiag_existsUnique_prime_dvd {d n p : ℕ} (hn : Squarefree n) (hp : p ∈ n.primeFactorsList)
(f : Fin d → ℕ) (hf : f ∈ finMulAntidiag d n) : ∃! i, p ∣ f i :=
by
rw [mem_finMulAntidiag] at hf
rw [mem_primeFactorsList hf.2, ← hf.1, hp.1.prime.dvd_finset_prod_iff] at hp
obtain ⟨i, his, hi⟩ := hp.2
refine ⟨i, hi, ?_⟩
intro j hj
by_contra hij
apply Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.1, hi, hj⟩
apply Nat.coprime_of_squarefree_mul
apply hn.squarefree_of_dvd
rw [← hf.1, ← Finset.mul_prod_erase _ _ his, ← Finset.mul_prod_erase _ _ (mem_erase.mpr ⟨hij, mem_univ _⟩), ←
mul_assoc]
apply Nat.dvd_mul_right
