zmodEquivZPowers_symm_apply_zpow'

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

URI: https://scilib.ai/kg/mathlib#IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow'

English

The same as above for a variant with unit coe.

Русский

То же самое для варианта с единичной вставкой.

LaTeX

$$h.zmodEquivZPowers.symm ⟨ζ^i, i, rfl⟩ = i$$

Lean4

@[simp]
theorem zmodEquivZPowers_symm_apply_zpow' (i : ℤ) : h.zmodEquivZPowers.symm ⟨ζ ^ i, i, rfl⟩ = i :=
  h.zmodEquivZPowers_symm_apply_zpow i

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

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

Разделы

Аффилиация

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