pow_mod_card

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#pow_mod_card

← MathLib Explorer

English

If gcd(|G|, n) = 1 then powCoprime h 1 = 1, i.e., 1 maps to 1 under the bijection.

Русский

Пусть gcd(|G|, n) = 1. Тогда powCoprime h 1 = 1.

LaTeX

$$powCoprime h 1 = 1$$

Lean4

@[to_additive (attr := simp) mod_card_nsmul]
theorem pow_mod_card (a : G) (n : ℕ) : a ^ (n % card G) = a ^ n := by
  rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, pow_mod_orderOf]

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

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

Разделы

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

Аффилиация

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