even_pow'

Mathlib.Algebra.Group.Nat.Even

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

English

If n ≠ 0, then m^n is even iff m is even.

Русский

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

LaTeX

$$$\text{If } n \neq 0:\; \operatorname{Even}(m^n) \iff \operatorname{Even}(m)$$$

Lean4

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

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

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

Разделы

Аффилиация

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