pow_apply — Mathlib

English

The explicit representation of the m-th power element in the submonoid generated by n is the pair (n^m, m) with the witness that it lies in powers(n).

Русский

Явное представление m-й степени элемента n в порожденном им подмножество состоит из пары (n^m, m) с доказательством принадлежности к powers(n).

LaTeX

$$$ \\text{pow}(n,m) = \\langle n^m, m, rfl \\rangle $$$

Lean4

theorem pow_apply (n : M) (m : ℕ) : Submonoid.pow n m = ⟨n ^ m, m, rfl⟩ :=
  rfl

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