pow_mem

Mathlib.Algebra.Ring.Subsemiring.Defs

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

English

If x is in a subsemiring s of a semiring R, then x^n is also in s for every natural n.

Русский

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

LaTeX

$$$\forall {R} [\text{Semiring } R] (s : \mathrm{Subsemiring}(R)) {x : R}, x \in s \rightarrow \forall n : \mathbb{N}, x^n \in s$$$

Lean4

protected theorem pow_mem {R : Type*} [Semiring R] (s : Subsemiring R) {x : R} (hx : x ∈ s) (n : ℕ) : x ^ n ∈ s :=
  pow_mem hx n

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

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

Разделы

Аффилиация

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