divInt_div_divInt_cancel_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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