natCast_ne

Mathlib.Data.Nat.Cast.NeZero

URI: https://scilib.ai/kg/mathlib#NeZero.natCast_ne

English

If n.cast is nonzero in R, then (n) cast in R is nonzero.

Русский

Если (n) в R не равен нулю, то само число n в R не равно нулю.

LaTeX

$$$ (n : R) \neq 0 $$$

Lean4

theorem natCast_ne (n : ℕ) (R) [AddMonoidWithOne R] [h : NeZero (n : R)] : (n : R) ≠ 0 :=
  h.out

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

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

Разделы

Аффилиация

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