English
For d, n, the image of finMulAntidiag under the projection to a single coordinate i is exactly the divisors of n, provided d ≠ 1.
Русский
Для d, n образ финMulAntidiag под проекцией к координате i даёт делители n при условии d ≠ 1.
LaTeX
$$$\text{image}_{i}(\text{finMulAntidiag}(d,n)) = \text{divisors}(n) \quad (d\neq 1)$$$
Lean4
theorem image_apply_finMulAntidiag {d n : ℕ} {i : Fin d} (hd : d ≠ 1) :
(finMulAntidiag d n).image (fun f => f i) = divisors n :=
by
ext k
simp only [mem_image, ne_eq, mem_divisors]
constructor
· rintro ⟨f, hf, rfl⟩
exact ⟨dvd_of_mem_finMulAntidiag hf _, (mem_finMulAntidiag.mp hf).2⟩
· simp_rw [mem_finMulAntidiag]
rintro ⟨⟨r, rfl⟩, hn⟩
have hs : Nontrivial (Fin d) := by
rw [Fin.nontrivial_iff_two_le]
obtain rfl | hd' := eq_or_ne d 0
· exact i.elim0
omega
obtain ⟨i', hi_ne⟩ := exists_ne i
use fun j => if j = i then k else if j = i' then r else 1
simp only [ite_true, and_true]
rw [← Finset.mul_prod_erase (h := mem_univ i), ← Finset.mul_prod_erase (a := i')]
· simp_all
exact mem_erase.mpr ⟨hi_ne, mem_univ _⟩
