zpow_eq_zpow_emod'

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#zpow_eq_zpow_emod'

English

Let x ∈ G, m ∈ ℤ, n ∈ ℕ with x^n = 1. Then x^m = x^{m mod (n)}.

Русский

Пусть x ∈ G, m ∈ ℤ, n ∈ ℕ, и x^n = 1. Тогда x^m = x^{m mod n}.

LaTeX

$$$\forall x \in G,\ \forall m \in \mathbb{Z},\ \forall n \in \mathbb{N},\ x^{n}=1 \Rightarrow x^{m} = x^{m\bmod n}$$$

Lean4

theorem zpow_eq_zpow_emod' {x : G} (m : ℤ) {n : ℕ} (h : x ^ n = 1) : x ^ m = x ^ (m % (n : ℤ)) :=
  zpow_eq_zpow_emod m (by simpa)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru