English
Let α be a Division Ring. If n divides m in the integers and n is nonzero in α, then the cast of m/n from ℤ to α equals m/n in α.
Русский
Пусть α — кольцо деления. Если n делит m в целых числах и (n : α) ≠ 0, то отображение m/n из ℤ в α равно m/n в α.
LaTeX
$$$ [DivisionRing α] \rightarrow \forall m,n \in \mathbb{Z},\ (n \mid m) \rightarrow (n : α) \neq 0 \rightarrow ((m / n : \mathbb{Z}) : α) = m / n.$$$
Lean4
@[simp]
theorem cast_div [DivisionRing α] {m n : ℤ} (n_dvd : n ∣ m) (hn : (n : α) ≠ 0) : ((m / n : ℤ) : α) = m / n :=
by
rcases n_dvd with ⟨k, rfl⟩
have : n ≠ 0 := by rintro rfl; simp at hn
rw [Int.mul_ediv_cancel_left _ this, mul_comm n, Int.cast_mul, mul_div_cancel_right₀ _ hn]
