English
Equivalently to map_nsmul_piAntidiag_univ, the image of the universal piAntidiag under the n-multiplication map coincides with the divisor-filtered universal piAntidiag.
Русский
Эквивалентно map_nsmul_piAntidiag_univ: образ универсального piAntidiag под отображением умножения на n совпадает с универcальным piAntidiag, отфильтрованным по делимости.
LaTeX
$$$\\text{map }\\langle n\\cdot \\_, \\_\\rangle (\\piAntidiag(\\mathrm{univ}, m)) = \\{ f \\in \\piAntidiag(\\mathrm{univ}, n m) \\mid \\forall i, n \\mid f(i) \\}$$$
Lean4
theorem map_nsmul_piAntidiag_univ [Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
(piAntidiag (univ : Finset ι) m).map ⟨(n • ·), fun _ _ h ↦ funext fun i ↦ mul_right_injective₀ hn (congr_fun h i)⟩ =
{f ∈ piAntidiag (univ : Finset ι) (n * m) | ∀ i, n ∣ f i} :=
by simpa using map_nsmul_piAntidiag (univ : Finset ι) m hn
