intCast_div — Mathlib

English

If a,b ∈ ℤ and b divides a, then the rational value of a/b coincides with the rational a/b.

Русский

Если a,b ∈ ℤ и b делит a, то значение в ℚ дроби a/b совпадает с рациональным a/b.

LaTeX

$$$\\forall a,b \\in \\mathbb{Z},\\ b \\mid a \\Rightarrow (a / b : \\mathbb{Q}) = a / b$$$

Lean4

theorem intCast_div (a b : ℤ) (h : b ∣ a) : ((a / b : ℤ) : ℚ) = a / b :=
  by
  rcases h with ⟨c, rfl⟩
  rw [mul_comm b, Int.mul_ediv_assoc c (dvd_refl b), Int.cast_mul, intCast_div_self, Int.cast_mul, mul_div_assoc]

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