pow

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Odd.pow

← MathLib Explorer

English

If a is odd, then a^n is odd for every exponent n.

Русский

Если a нечетно, то a^n нечетно для любого показателя n.

LaTeX

$$$\forall n:\\mathbb{N},\ \operatorname{Odd}(a) \rightarrow \operatorname{Odd}(a^{n})$$$

Lean4

theorem pow {n : ℕ} (ha : Odd a) : Odd (a ^ n) := by
  induction n with
  | zero => simp [pow_zero]
  | succ n hrec => rw [pow_succ]; exact hrec.mul ha

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

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

Разделы

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

Аффилиация

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