zmodChar_apply'

Mathlib.NumberTheory.LegendreSymbol.AddCharacter

URI: https://scilib.ai/kg/mathlib#AddChar.zmodChar_apply'

← MathLib Explorer

English

For n > 0 and a ∈ ℕ, zmodChar n hζ a = ζ^{a}.

Русский

Для натурального a и n>0: zmodChar n hζ a = ζ^{a}.

LaTeX

$$zmodChar(n,hζ)(a) = ζ^{a}$$

Lean4

theorem zmodChar_apply' {n : ℕ} [NeZero n] {ζ : C} (hζ : ζ ^ n = 1) (a : ℕ) : zmodChar n hζ a = ζ ^ a := by
  rw [pow_eq_pow_mod a hζ, zmodChar_apply, ZMod.val_natCast]

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

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

Разделы

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

Аффилиация

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