pos_of_isNat

Mathlib.Tactic.Positivity.Core

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.Positivity.pos_of_isNat

Lean4

theorem pos_of_isNat {n : ℕ} [Semiring A] [PartialOrder A] [IsOrderedRing A] [Nontrivial A] (h : NormNum.IsNat e n)
    (w : Nat.ble 1 n = true) : 0 < (e : A) :=
  by
  rw [NormNum.IsNat.to_eq h rfl]
  apply Nat.cast_pos.2
  simpa using w

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

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

Разделы

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

Аффилиация

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