zsmul_mem

Mathlib.RingTheory.NonUnitalSubring.Defs

URI: https://scilib.ai/kg/mathlib#NonUnitalSubring.zsmul_mem

English

If x ∈ s then n • x ∈ s for all integers n.

Русский

Если x ∈ s, то для любого целого n верно n • x ∈ s.

LaTeX

$$$ x \in s \Rightarrow \forall n \in \mathbb{Z}, n \cdot x \in s $$$

Lean4

protected theorem zsmul_mem {x : R} (hx : x ∈ s) (n : ℤ) : n • x ∈ s :=
  zsmul_mem hx n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru