ofNat_pos'

Mathlib.Data.Nat.Cast.Order.Ring

URI: https://scilib.ai/kg/mathlib#Nat.ofNat_pos'

← MathLib Explorer

English

For {n} with [n.AtLeastTwo], 0 < (ofNat(n) : α).

Русский

Для {n} с [n.AtLeastTwo] выполняется 0 < (ofNat(n) : α).

LaTeX

$$$0 < (\mathrm{ofNat}(n) : \alpha)$$$

Lean4

/-- See also `Nat.ofNat_pos`, specialised for an `OrderedSemiring`. -/
@[simp low]
theorem ofNat_pos' {n : ℕ} [n.AtLeastTwo] : 0 < (ofNat(n) : α) :=
  cast_pos'.mpr (NeZero.pos n)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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