instNeZeroHAddNatOfNat_mathlib_1

Mathlib.Data.ZMod.Defs

URI: https://scilib.ai/kg/mathlib#Fin.instNeZeroHAddNatOfNat_mathlib_1

English

If n ≠ 0, then the element 1 in Fin(n+1) is nonzero.

Русский

Если n ≠ 0, то единица в Fin(n+1) не равна нулю.

LaTeX

$$$\forall n \,(n \neq 0) \Rightarrow (1 : Fin(n+1)) \neq 0.$$$

Lean4

instance (n : ℕ) [NeZero n] : NeZero (1 : Fin (n + 1)) :=
  open Fin.CommRing in inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru