inv_def

Mathlib.Algebra.Field.Rat

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

English

For q ∈ ℚ≥0, q⁻1 is the rational with numerator q.den and denominator q.num, i.e. q⁻1 = divNat(q.den, q.num).

Русский

Для q ∈ ℚ≥0 обратное q равно числителю q.den и знаменателю q.num, то есть q⁻1 = divNat(q.den, q.num).

LaTeX

$$$ q^{-1} = \operatorname{divNat}(q.\den, q.\num) $$$

Lean4

theorem inv_def (q : ℚ≥0) : q⁻¹ = divNat q.den q.num := by ext; simp [Rat.inv_def, num_coe, den_coe]

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

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

Разделы

Аффилиация

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