zpow — Mathlib

English

A subgroup is closed under integer powers: for any a ∈ H and n ∈ ℤ, a^n ∈ H.

Русский

Подгруппа замкнута относительно целых степеней: для любого a ∈ H и n ∈ ℤ, 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 {M S} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} : Pow H ℤ :=
  ⟨fun a n => ⟨a.1 ^ n, zpow_mem a.2 n⟩⟩

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