mk_pow — Mathlib

English

Within a submonoid S, if x ∈ M with hx ∈ S, then (⟨x, hx⟩ : S)^n = ⟨x^n, pow_mem hx n⟩ for all n.

Русский

Внутри подмоноида S, если x ∈ M и hx ∈ S, то (⟨x, hx⟩ : S)^n = ⟨x^n, pow_mem hx n⟩ для всех n.

LaTeX

$$$\forall (x : M) (hx : x \in S) (n : \mathbb{N}), (⟨x, hx⟩ : S)^n = ⟨x^n, pow_mem hx n⟩$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_pow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : M) (hx : x ∈ S) (n : ℕ) :
    (⟨x, hx⟩ : S) ^ n = ⟨x ^ n, pow_mem hx n⟩ :=
  rfl

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