divInt_div_divInt_cancel_right — Mathlib

English

Let x ∈ ℤ, x ≠ 0. For all n,d ∈ ℤ, (x/n)/(x/d) = d/n in ℚ.

Русский

Пусть x ∈ ℤ, x ≠ 0. Для любых n,d ∈ ℤ верно (x/n)/(x/d) = d/n в ℚ.

LaTeX

$$$\forall x \in \mathbb{Z}, x \neq 0 \; \forall n,d \in \mathbb{Z}, \; \frac{x/n}{x/d} = \frac{d}{n}$$$

Lean4

theorem divInt_div_divInt_cancel_right {x : ℤ} (hx : x ≠ 0) (n d : ℤ) : x /. n / (x /. d) = d /. n := by
  rw [div_eq_mul_inv, inv_divInt, mul_comm, divInt_mul_divInt_cancel hx]

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