zpow_odd

Mathlib.Data.Sign.Basic

URI: https://scilib.ai/kg/mathlib#SignType.zpow_odd

← MathLib Explorer

English

For SignType and odd integer z, s^z = s.

Русский

Для SignType и нечётного целого z выполняется s^z = s.

LaTeX

$$$\forall s:\; SignType,\; Odd(z) \Rightarrow s^z = s$$$

Lean4

theorem zpow_odd (s : SignType) {z : ℤ} (hz : Odd z) : s ^ z = s :=
  by
  obtain rfl | hs := eq_or_ne s 0
  · rw [zero_zpow]
    rintro rfl
    simp at hz
  obtain ⟨k, rfl⟩ := hz
  rw [zpow_add₀ hs, zpow_one, zpow_mul, zpow_two]
  cases s <;> simp

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

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

Разделы

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

Аффилиация

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