even_pow

Mathlib.Algebra.Group.Nat.Even

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

← MathLib Explorer

English

m^n is even iff m is even and n > 0.

Русский

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

LaTeX

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

Lean4

/-- If `m` and `n` are natural numbers, then the natural number `m^n` is even
if and only if `m` is even and `n` is positive. -/
@[parity_simps, grind =]
theorem even_pow : Even (m ^ n) ↔ Even m ∧ n ≠ 0 := by induction n with grind

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

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

Разделы

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

Аффилиация

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