toNNRat_inv — Mathlib

English

For q ∈ ℚ, the map to NN rational commutes with inversion: toNNRat(q^{-1}) = (toNNRat q)^{-1}.

Русский

Преобразование к ℕН дроби сохраняет операцию взятия обратного: toNNRat(q^{-1}) = (toNNRat q)^{-1}.

LaTeX

$$toNNRat(q^{-1}) = (toNNRat q)^{-1}$$

Lean4

theorem toNNRat_inv (q : ℚ) : toNNRat q⁻¹ = (toNNRat q)⁻¹ :=
  by
  obtain hq | hq := le_total q 0
  · rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]
  · nth_rw 1 [← Rat.coe_toNNRat q hq]
    rw [← coe_inv, toNNRat_coe]

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