one_le

Mathlib.Data.Nat.Cast.NeZero

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

English

If n is a nonzero natural, then 1 ≤ n.

Русский

Если n не равно нулю, то 1 ≤ n.

LaTeX

$$$1 \le n$$$

Lean4

theorem one_le {n : ℕ} [NeZero n] : 1 ≤ n := by have := NeZero.ne n; cutsat

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

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

Разделы

Аффилиация

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