element_of_chain_not_isUnit_of_index_ne_zero

English

In a divisor chain c: Fin(n+1) → Associates(M) that enumerates divisors of q, every nonzero index i ≠ 0 yields c(i) not a unit.

Русский

В цепи делителей c: Fin(n+1) → Associates(M), перечисляющей делители q, каждый индекс i ≠ 0 имеет свой элемент c(i), не являющийся единицей.

LaTeX

$$$\forall n\,\forall i:\mathrm{Fin}(n+1),\ i \neq 0 \Rightarrow \neg \mathrm{IsUnit}(c(i))$$$

Lean4

theorem element_of_chain_not_isUnit_of_index_ne_zero {n : ℕ} {i : Fin (n + 1)} (i_pos : i ≠ 0)
    {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c) : ¬IsUnit (c i) :=
  DvdNotUnit.not_unit
    (Associates.dvdNotUnit_iff_lt.2 (h₁ <| show (0 : Fin (n + 1)) < i from Fin.pos_iff_ne_zero.mpr i_pos))

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