intCast_div_mul_eq_zsmul — Mathlib

English

For any integer m, the zsmul version of the division-multiplication identity holds in AddCircle(p): the image of ↑(↑m/q·r) equals m times (r/q) in AddCircle(p).

Русский

Для целого m выполнено тождество в AddCircle(p): образ ↑(↑m/q·r) равен m умножению на (r/q) в AddCircle(p).

LaTeX

$$$\uparrow\left(\dfrac{m}{q} r\right) = m \cdot \left(\dfrac{r}{q}\right) \text{ in } \mathrm{AddCircle}(p)$$

Lean4

theorem intCast_div_mul_eq_zsmul (r : 𝕜) (m : ℤ) : (↑(↑m / q * r) : AddCircle p) = m • (r / q : AddCircle p) := by
  rw [mul_comm_div, ← zsmul_eq_mul, coe_zsmul]

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