even_pow

Mathlib.Algebra.Group.Int.Even

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

English

For m ∈ ℤ and n ∈ ℕ, m^n is even iff m is even and n ≠ 0.

Русский

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

LaTeX

$$$$ \operatorname{Even}(m^n) \iff (\operatorname{Even}(m) \land n \neq 0). $$$$

Lean4

@[parity_simps, grind =]
theorem even_pow {n : ℕ} : Even (m ^ n) ↔ Even m ∧ n ≠ 0 := by induction n with grind

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

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

Разделы

Аффилиация

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