of_neZero_natCast

Mathlib.Data.Nat.Cast.NeZero

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

English

From NeZero (n.cast) we deduce NeZero n.

Русский

Из NeZero (n.cast) следует NeZero n.

LaTeX

$$$ [\text{NeZero} (n \;:\; R)] \Rightarrow \text{NeZero} n $$$

Lean4

theorem of_neZero_natCast (R) [AddMonoidWithOne R] {n : ℕ} [h : NeZero (n : R)] : NeZero n :=
  ⟨by rintro rfl; exact h.out Nat.cast_zero⟩

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

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

Разделы

Аффилиация

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