pow

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.ModEq.pow

← MathLib Explorer

English

If a ≡ b (mod n), then a^m ≡ b^m (mod n) for any natural exponent m.

Русский

Если a ≡ b (mod n), то a^m ≡ b^m (mod n) для любого натурального показателя m.

LaTeX

$$$a \equiv b \pmod n \Rightarrow a^m \equiv b^m \pmod n$$$

Lean4

@[gcongr]
protected theorem pow (m : ℕ) (h : a ≡ b [ZMOD n]) : a ^ m ≡ b ^ m [ZMOD n] := by
  induction m with
  | zero => rfl
  | succ d hd => rw [pow_succ, pow_succ]; exact hd.mul h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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