ne_zero_of_mem_finMulAntidiag — Mathlib

English

If f ∈ finMulAntidiag d n, then every component f(i) is nonzero.

Русский

Если f ∈ finMulAntidiag d n, то все компонентные значения f(i) ненулевые.

LaTeX

$$$f\in\text{finMulAntidiag}(d,n)\Rightarrow ∀ i, f(i)\neq 0$$$

Lean4

theorem ne_zero_of_mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} (hf : f ∈ finMulAntidiag d n) (i : Fin d) : f i ≠ 0 :=
  ne_zero_of_dvd_ne_zero (mem_finMulAntidiag.mp hf).2 (dvd_of_mem_finMulAntidiag hf i)

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