cast_pos_of_pos

Mathlib.Data.Rat.Cast.Order

URI: https://scilib.ai/kg/mathlib#Rat.cast_pos_of_pos

← MathLib Explorer

English

If q > 0 in Rat, then its image in any ordered field K is positive: 0 < (q : K).

Русский

Если q > 0 в Rat, то его образ в любом упорядоченном поле K положителен: 0 < (q : K).

LaTeX

$$$ ∀ {q : \mathrm{Rat}} [..], \ q > 0 \implies 0 < (q : K). $$$

Lean4

theorem cast_pos_of_pos (hq : 0 < q) : (0 : K) < q :=
  by
  rw [Rat.cast_def]
  exact div_pos (Int.cast_pos.2 <| num_pos.2 hq) (Nat.cast_pos.2 q.pos)

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

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

Разделы

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

Аффилиация

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