divInt_mul_divInt_cancel

Mathlib.Data.Rat.Defs

URI: https://scilib.ai/kg/mathlib#Rat.divInt_mul_divInt_cancel

← MathLib Explorer

English

For x ∈ ℤ with x ≠ 0 and integers n, d, we have (n/x) * (x/d) = n/d.

Русский

Для x ∈ ℤ, x ≠ 0, и целых n, d верно (n/x) · (x/d) = n/d.

LaTeX

$$$x \in \mathbb{Z}, x \neq 0 \Rightarrow (n / x) \cdot (x / d) = n / d$$$

Lean4

theorem divInt_mul_divInt_cancel {x : ℤ} (hx : x ≠ 0) (n d : ℤ) : n /. x * (x /. d) = n /. d :=
  by
  by_cases hd : d = 0
  · rw [hd]
    simp
  rw [divInt_mul_divInt, x.mul_comm, divInt_mul_right hx]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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