pow_left

Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

URI: https://scilib.ai/kg/mathlib#jacobiSym.pow_left

← MathLib Explorer

English

For all a ∈ ℤ and e,b ∈ ℕ, J(a^e | b) = J(a | b)^e.

Русский

Для любых a ∈ ℤ и e,b ∈ ℕ выполняется J(a^e | b) = J(a | b)^e.

LaTeX

$$$ J(a^e | b) = J(a | b)^e $$$

Lean4

/-- We have that `J(a^e | b) = J(a | b)^e`. -/
theorem pow_left (a : ℤ) (e b : ℕ) : J(a ^ e | b) = J(a | b) ^ e :=
  Nat.recOn e (by rw [_root_.pow_zero, _root_.pow_zero, one_left]) fun _ ih => by
    rw [_root_.pow_succ, _root_.pow_succ, mul_left, ih]

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

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

Разделы

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

Аффилиация

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