npow — Mathlib

English

If H is a Subgroup of G, then H is closed under natural powers: for any a in H and n in N, a^n ∈ H.

Русский

Если H — подгруппа G, то она замкнута относительно натуральных степеней: для любого a ∈ H и n ∈ ℕ имеется a^n ∈ H.

LaTeX

$$$\forall a \in H,\\forall n \in \mathbb{N}, a^{n} \in H$$$

Lean4

/-- A subgroup of a group inherits a natural power -/
@[to_additive existing]
protected instance npow : Pow H ℕ :=
  ⟨fun a n => ⟨a ^ n, H.pow_mem a.2 n⟩⟩

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