intCast_mul_mem_zmultiples — Mathlib

English

In a ring, for any r and integer k, the element (k as integer) times r lies in zmultiples r: ↑(k : ℤ) * r ∈ zmultiples r.

Русский

В кольце для любого r и целого k элемент k·r принадлежит zmultiples r.

LaTeX

$$$\uparrow(k : \mathbb Z) \cdot r \in \operatorname{zmultiples}(r)$$$

Lean4

@[simp]
theorem intCast_mul_mem_zmultiples : ↑(k : ℤ) * r ∈ zmultiples r := by
  simpa only [← zsmul_eq_mul] using zsmul_mem_zmultiples r k

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