inv_mkRat

Mathlib.Data.Rat.Defs

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

English

The inverse of mkRat a b is b /. a.

Русский

Обратное mkRat a b равно b /. a.

LaTeX

$$$ (mkRat a b)^{-1} = b /. a $$$

Lean4

@[simp]
theorem inv_mkRat (a : ℤ) (b : ℕ) : (mkRat a b)⁻¹ = b /. a := by rw [mkRat_eq_divInt, inv_divInt]

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

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

Разделы

Аффилиация

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