num_denom_neg

Mathlib.FieldTheory.RatFunc.Basic

URI: https://scilib.ai/kg/mathlib#RatFunc.num_denom_neg

← MathLib Explorer

English

Iff (x.num · q) = (p · x.denom) then x = p/q for q ≠ 0.

Русский

Если x.num · q = p · x.denom, то x = p/q при q ≠ 0.

LaTeX

$$$q \neq 0 \Rightarrow (x.num \cdot q = p \cdot x.denom) \iff x = \dfrac{p}{q}$$$

Lean4

theorem num_denom_neg (x : RatFunc K) : (-x).num * x.denom = -x.num * (-x).denom := by
  rw [num_mul_eq_mul_denom_iff (denom_ne_zero x), map_neg, neg_div, num_div_denom]

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

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

Разделы

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

Аффилиация

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