nsmul_piAntidiag_univ — Mathlib

English

As a corollary of nsmul_piAntidiag_univ, the n-fold multiple of the universal piAntidiag equals the filter of univ piAntidiag by divisibility on every coordinate.

Русский

Как следствие из nsmul_piAntidiag_univ, n-раз кратное от универсального piAntidiag равно фильтруемому по делимости на каждом координате piAntidiag на унив.

LaTeX

$$$n\\cdot \\mathbb{N}\\text{-}\\pi\\mathrm{Antidiag}(\\mathrm{univ}, m) = \\{ f \\in \\piAntidiag(\\mathrm{univ}, n\\cdot m) \\mid \\forall i, n \\mid f(i) \\}$$$

Lean4

theorem nsmul_piAntidiag_univ [Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
    n•ℕ(piAntidiag univ m) = {f ∈ piAntidiag (univ : Finset ι) (n * m) | ∀ i, n ∣ f i} := by
  simpa using nsmul_piAntidiag (univ : Finset ι) m hn

Похожие утверждения