χ₈'_int_eq_χ₄_mul_χ₈

Mathlib.NumberTheory.LegendreSymbol.ZModChar

URI: https://scilib.ai/kg/mathlib#ZMod.χ₈'_int_eq_χ₄_mul_χ₈

English

For any integer a, χ8'(a) = χ4(a) χ8(a).

Русский

Для любого целого a выполняется χ8'(a) = χ4(a) χ8(a).

LaTeX

$$$$\forall a \in \mathbb{Z}, \ χ_8'(a)=χ_4(a)\,χ_8(a).$$$$

Lean4

theorem χ₈'_int_eq_χ₄_mul_χ₈ (a : ℤ) : χ₈' a = χ₄ a * χ₈ a :=
  by
  rw [← @cast_intCast 8 (ZMod 4) _ 4 _ (by cutsat) a]
  exact χ₈'_eq_χ₄_mul_χ₈ a

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

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

Разделы

Аффилиация

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