num_divNat_den

Mathlib.Data.NNRat.Defs

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

English

For any q ∈ ℚ≥0, the NRat divNat q.num q.den equals q.

Русский

Для любого q ∈ ℚ≥0, divNat q.num q.den равно q.

LaTeX

$$$ divNat q.num q.den = q $$$

Lean4

@[simp]
theorem num_divNat_den (q : ℚ≥0) : divNat q.num q.den = q :=
  ext <| by rw [← (q : ℚ).mkRat_num_den']; simp [num_coe, den_coe]

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

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

Разделы

Аффилиация

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