even_pow'

Mathlib.Algebra.Group.Int.Even

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

English

If n ≠ 0, then for m ∈ ℤ and n ∈ ℕ, m^n is even iff m is even.

Русский

Если n ≠ 0, то для m ∈ ℤ и n ∈ ℕ, m^n чётно тогда и только тогда, когда m чётно.

LaTeX

$$$$ \forall m \in \mathbb{Z}, \forall n \in \mathbb{N}, n \neq 0 \Rightarrow \operatorname{Even}(m^n) \iff \operatorname{Even}(m). $$$$

Lean4

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

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

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

Разделы

Аффилиация

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