mkRat_eq_divInt

Mathlib.Data.Rat.Defs

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

English

For any integer n and natural d, mkRat n d equals n /. d.cast.

Русский

Для любых целого n и натурального d число mkRat n d эквивалентно отношению n / d.

LaTeX

$$$ \forall (n : \mathbb{Z}) (d : \mathbb{N}), mkRat n d = n /. (d : \mathbb{Z}) $$$

Lean4

theorem mkRat_eq_divInt (n d) : mkRat n d = n /. d :=
  rfl

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

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

Разделы

Аффилиация

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