cons_pos

Mathlib.Tactic.FieldSimp.Lemmas

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.FieldSimp.NF.cons_pos

Lean4

theorem cons_pos [GroupWithZero M] [PartialOrder M] [PosMulStrictMono M] [PosMulReflectLT M] [ZeroLEOneClass M] (r : ℤ)
    {x : M} (hx : 0 < x) {l : NF M} (hl : 0 < l.eval) : 0 < ((r, x) ::ᵣ l).eval :=
  by
  unfold eval cons
  apply mul_pos ?_ hl
  simp only
  rw [zpow'_of_ne_zero_left _ _ hx.ne']
  apply zpow_pos hx

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

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

Разделы

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

Аффилиация

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