nPow — Mathlib

English

A submonoid S of a Monoid M carries a power operator: for every element p ∈ S and n ∈ ℕ, p^n ∈ S.

Русский

Подмножество S подмноида M поддерживает возведение в натуральные степени: для каждого p ∈ S и n ∈ ℕ верно p^n ∈ S.

LaTeX

$$$\forall (p : S) (n : \mathbb{N}), (p^n) \in S$$$

Lean4

/-- A submonoid of a monoid inherits a power operator. -/
instance nPow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) : Pow S ℕ :=
  ⟨fun a n => ⟨a.1 ^ n, pow_mem a.2 n⟩⟩

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