div_def

Mathlib.Algebra.Field.Rat

URI: https://scilib.ai/kg/mathlib#NNRat.div_def

English

Let p,q ∈ ℚ≥0. Then p/q equals divNat(p.num · q.den, p.den · q.num).

Русский

Пусть p,q ∈ ℚ≥0. Тогда p/q = divNat(p.num · q.den, p.den · q.num).

LaTeX

$$$ p/q = \operatorname{divNat} (p.\num \cdot q.\den) (p.\den \cdot q.\num) $$$

Lean4

theorem div_def (p q : ℚ≥0) : p / q = divNat (p.num * q.den) (p.den * q.num) := by ext;
  simp [Rat.div_def', num_coe, den_coe]

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

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

Разделы

Аффилиация

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