even_coe_nat — Mathlib

English

Let n be a natural number. Then n is even as an integer if and only if n is even as a natural number.

Русский

Пусть n ∈ ℕ. Тогда n чётно как целое число тогда и только тогда, когда n чётно как натуральное число.

LaTeX

$$$\\forall n \\\in \\mathbb{N},\\ \operatorname{Even}(n:\\mathbb{Z}) \\\iff \\operatorname{Even}(n)$$$

Lean4

@[simp, norm_cast, grind =]
theorem even_coe_nat (n : ℕ) : Even (n : ℤ) ↔ Even n := by rw_mod_cast [even_iff, Nat.even_iff]

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