dvd_of_mem_finMulAntidiag — Mathlib

English

If f ∈ finMulAntidiag d n, then for every i, f(i) divides n.

Русский

Если f ∈ finMulAntidiag d n, то для каждого i значение f(i) делит n.

LaTeX

$$$f\in\text{finMulAntidiag}(d,n)\Rightarrow \forall i, f(i) \mid n$$$

Lean4

theorem dvd_of_mem_finMulAntidiag {n d : ℕ} {f : Fin d → ℕ} (hf : f ∈ finMulAntidiag d n) (i : Fin d) : f i ∣ n :=
  by
  rw [mem_finMulAntidiag] at hf
  rw [← hf.1]
  exact dvd_prod_of_mem f (mem_univ i)

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