χ₈'_eq_χ₄_mul_χ₈

Mathlib.NumberTheory.LegendreSymbol.ZModChar

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

English

The character χ8' factors as the product of the characters χ4 and χ8 on the group Z/8Z.

Русский

Символ χ8' раскладывается как произведение χ4 и χ8 на группе Z/8Z.

LaTeX

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

Lean4

/-- The relation between `χ₄`, `χ₈` and `χ₈'` -/
theorem χ₈'_eq_χ₄_mul_χ₈ : ∀ a : ZMod 8, χ₈' a = χ₄ (cast a) * χ₈ a := by decide

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

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

Разделы

Аффилиация

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