natCast_div_mul_eq_nsmul — Mathlib

English

In AddCircle(p), the natural cast relation expresses that ↑m/q·r equals m times (r/q) in the circle for natural m.

Русский

В AddCircle(p) естественное отображение чисел устанавливает, что численно m/q·r в окружности равно m раз (r/q) в окружности.

LaTeX

$$$\uparrow\left(\frac{m}{q} r\right) = m \;\big(\frac{r}{q}\big) \quad \text{in } \mathrm{AddCircle}(p)$$$

Lean4

theorem natCast_div_mul_eq_nsmul (r : 𝕜) (m : ℕ) : (↑(↑m / q * r) : AddCircle p) = m • (r / q : AddCircle p) := by
  rw [mul_comm_div, ← nsmul_eq_mul, coe_nsmul]

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