English
Applying a scalar multiplication map to piAntidiag over univ yields the same target as filtering by divisibility, aligning with the n-division condition across all coordinates.
Русский
Применение отображения умножения на piAntidiag на унив приводит к тому же множеству, что и фильтрация по делимости, согласуясь с условием делимости по всем координатам.
LaTeX
$$$\\text{map }(\\lambda x. n\\cdot x)(\\piAntidiag(\\mathrm{univ}, m)) = \\{ f \\in \\piAntidiag(\\mathrm{univ}, n\\cdot m) \\mid \\forall i, n \\mid f(i) \\}$$$
Lean4
theorem map_nsmul_piAntidiag (s : Finset ι) (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
(piAntidiag s m).map ⟨(n • ·), fun _ _ h ↦ funext fun i ↦ mul_right_injective₀ hn (congr_fun h i)⟩ =
{f ∈ piAntidiag s (n * m) | ∀ i ∈ s, n ∣ f i} :=
by classical rw [map_eq_image]; exact nsmul_piAntidiag _ _ hn
