int_mul_mem — Mathlib

English

In any additive subgroup G of a ring, integer multiplication preserves membership: k*g ∈ G for any k ∈ ℤ and g ∈ G.

Русский

В любой аддитивной подгруппе G кольца целочисленное умножение сохраняет принадлежность: k·g ∈ G для любого k ∈ ℤ и g ∈ G.

LaTeX

$$$\forall k\in \mathbb{Z},\; \forall g\in G:\ (k\cdot g)\in G$$$

Lean4

theorem int_mul_mem {G : AddSubgroup R} (k : ℤ) {g : R} (h : g ∈ G) : (k : R) * g ∈ G :=
  by
  convert AddSubgroup.zsmul_mem G h k using 1
  rw [zsmul_eq_mul]

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