pow_mem — Mathlib

English

For any Submonoid M and x ∈ M, if x ∈ S then x^n ∈ S for all n ∈ ℕ; i.e., S is closed under taking powers.

Русский

Для любого Submonoid M и x ∈ M, если x ∈ S, то x^n ∈ S для всех n ∈ ℕ; то есть S замкнут относительно степеней.

LaTeX

$$$\forall (S : \mathrm{Submonoid} M) (x : M), x \in S \Rightarrow \forall n \in \mathbb{N}, x^n \in S$$$

Lean4

@[to_additive]
protected theorem pow_mem {M : Type*} [Monoid M] (S : Submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S :=
  pow_mem hx n

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