coe_inv

Mathlib.Algebra.Field.Rat

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

English

For q ∈ ℚ≥0, ((q^{-1}) : ℚ) = (q : ℚ)^{-1}.

Русский

Для q ∈ ℚ>=0, ((q^{-1}) : ℚ) = (q : ℚ)^{-1}.

LaTeX

$$$((q^{-1} : \mathbb{Q}_{\ge 0}) : \mathbb{Q}) = (q : \mathbb{Q})^{-1}$$$

Lean4

@[simp, norm_cast]
theorem coe_inv (q : ℚ≥0) : ((q⁻¹ : ℚ≥0) : ℚ) = (q : ℚ)⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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