odd_pow — Mathlib

English

For a natural exponent n, Odd(m^n) holds iff m is Odd or n = 0.

Русский

Для натурального показателя n нечетность m^n равна истинной тогда и только тогда, когда m нечетно либо n = 0.

LaTeX

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

Lean4

@[parity_simps]
theorem odd_pow {n : ℕ} : Odd (m ^ n) ↔ Odd m ∨ n = 0 := by grind

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