ofNat_nonneg — Mathlib

English

If α is a Semiring with partial order and IsOrderedRing, then for any n with [n.AtLeastTwo], 0 ≤ (ofNat(n) : α).

Русский

Пусть α — полупринужденная колец с частичным порядком; тогда для любого n с [n.AtLeastTwo] выполняется 0 ≤ (ofNat(n) : α).

LaTeX

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

Lean4

/-- Specialisation of `Nat.ofNat_nonneg'`, which seems to be easier for Lean to use. -/
@[simp]
theorem ofNat_nonneg {α} [Semiring α] [PartialOrder α] [IsOrderedRing α] (n : ℕ) [n.AtLeastTwo] : 0 ≤ (ofNat(n) : α) :=
  ofNat_nonneg' n

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