coe_divNat

Mathlib.Data.NNRat.Defs

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

English

The embedding of divNat(n,d) into the rationals yields the standard fraction n/d.

Русский

Встраивание divNat(n,d) в ℚ даёт обычную дробь n/d.

LaTeX

$$$ (divNat(n,d) : \mathbb{Q}) = \tfrac{n}{d} $$$

Lean4

@[simp, norm_cast]
theorem coe_divNat (n d : ℕ) : (divNat n d : ℚ) = .divInt n d :=
  rfl

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

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

Разделы

Аффилиация

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