even_iff_of_even — Mathlib

English

If n is even, then k is even iff k.val is even.

Русский

Если n четно, то k чётно тогда и только тогда, когда k.val чётно.

LaTeX

$$$\\forall n:\\mathbb{N},\\; \\mathrm{Even}\\,n\\Rightarrow \\mathrm{Even}(k) \\iff \\mathrm{Even}(k.\\mathrm{val}).$$$

Lean4

theorem even_iff_of_even (hn : Even n) : Even k ↔ Even k.val :=
  by
  rcases hn with ⟨n, rfl⟩
  refine ⟨?_, even_of_val⟩
  rintro ⟨l, rfl⟩
  rw [val_add_eq_ite]
  split_ifs with h <;> simp [Nat.even_sub, *]

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