cast_ne_zero

Mathlib.Algebra.CharZero.Defs

URI: https://scilib.ai/kg/mathlib#Nat.cast_ne_zero

English

For any n ∈ ℕ, (n : R) ≠ 0 iff n ≠ 0.

Русский

Для любого n ∈ ℕ, (n в R) ≠ 0 тогда и только тогда, что n ≠ 0.

LaTeX

$$(n : R) ≠ 0 \\\\iff n ≠ 0$$

Lean4

@[norm_cast]
theorem cast_ne_zero {n : ℕ} : (n : R) ≠ 0 ↔ n ≠ 0 :=
  not_congr cast_eq_zero

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

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

Разделы

Аффилиация

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