zpow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- A subgroup of a group inherits an integer power -/
@[to_additive existing]
instance zpow : Pow H ℤ :=
  ⟨fun a n => ⟨a ^ n, H.zpow_mem a.2 n⟩⟩

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