even_or_odd

Mathlib.NumberTheory.DirichletCharacter.Basic

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.even_or_odd

← MathLib Explorer

English

For any ψ on S, m, with NoZeroDivisors S, either ψ.Even or ψ.Odd holds.

Русский

Для любого ψ над S, m, при отсутствии нулевых делителей, выполняется либо ψ.Even, либо ψ.Odd.

LaTeX

$$$\\psi.Even \\lor \\psi.Odd,$$$

Lean4

theorem even_or_odd [NoZeroDivisors S] : ψ.Even ∨ ψ.Odd :=
  by
  suffices ψ (-1) ^ 2 = 1 by convert sq_eq_one_iff.mp this
  rw [← map_pow _, neg_one_sq, map_one]

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

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

Разделы

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

Аффилиация

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