intCast_mem_zmultiples_one — Mathlib

English

Let R be a ring. For every integer k, the element obtained by viewing k as an element of R lies in the additive subgroup zmultiples(1) (i.e., the subgroup generated by the unit 1).

Русский

Пусть R — кольцо. Для любого целого k элемент, получаемый как образ k в R, принадлежит подгруппе zmultiples(1) (то есть порождаемой единицей).

LaTeX

$$$(k : R) \in \operatorname{zmultiples}(1 : R)$$$

Lean4

@[simp]
theorem intCast_mem_zmultiples_one : ↑(k : ℤ) ∈ zmultiples (1 : R) :=
  mem_zmultiples_iff.mp ⟨k, by simp⟩

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