instNeZeroHAddNatOfNat_mathlib — Mathlib

English

Let n ≠ 0 and m ≠ 0. Then the element of Fin(n + ofNat(m)) corresponding to ofNat(m) is nonzero.

Русский

Пусть n ≠ 0 и m ≠ 0. Тогда элемент Fin(n + ofNat(m)), соответствующий ofNat(m), ненулевой.

LaTeX

$$$ (n \neq 0) \land (m \neq 0) \Rightarrow (ofNat(m) : \mathrm{Fin}(n + ofNat(m))) \neq 0 $$$

Lean4

instance [NeZero n] [NeZero ofNat(m)] : NeZero (ofNat(m) : Fin (n + ofNat(m))) :=
  by
  suffices m % (n + m) = m by simpa [neZero_iff, Fin.ext_iff, OfNat.ofNat, this] using NeZero.ne m
  apply Nat.mod_eq_of_lt
  simpa using zero_lt_of_ne_zero (NeZero.ne n)

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