odd_pow'

Mathlib.Algebra.Ring.Int.Parity

URI: https://scilib.ai/kg/mathlib#Int.odd_pow'

English

If the exponent n is nonzero, then Odd(m^n) iff Odd(m).

Русский

Если показатель степени n не равен нулю, то Odd(m^n) эквивалентно Odd(m).

LaTeX

$$$\\forall {m} {n : \\mathbb{N}}, n \neq 0 \\rightarrow \\operatorname{Odd}(m^n) \\iff \\operatorname{Odd} m$$$

Lean4

theorem odd_pow' {n : ℕ} (h : n ≠ 0) : Odd (m ^ n) ↔ Odd m := by grind

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

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

Разделы

Аффилиация

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