nsmul_mem

Mathlib.Algebra.Ring.Subsemiring.Defs

URI: https://scilib.ai/kg/mathlib#Subsemiring.nsmul_mem

English

If x ∈ s, then n • x ∈ s for all n ∈ ℕ.

Русский

Если x ∈ s, то n • x ∈ s для всех n ∈ ℕ.

LaTeX

$$$\forall {x : R} (hx : x \in s) (n : \mathbb{N}), n \cdot x \in s$$$

Lean4

protected theorem nsmul_mem {x : R} (hx : x ∈ s) (n : ℕ) : n • x ∈ s :=
  nsmul_mem hx n

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

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

Разделы

Аффилиация

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