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 : ℕ} [AddMonoidWithOne A] [PartialOrder A] [AddLeftMono A] [ZeroLEOneClass A]
    [h'' : NeZero (1 : 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