odd_iff_of_even — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem odd_iff_of_even [NeZero n] (hn : Even n) : Odd k ↔ Odd k.val :=
  by
  rcases hn with ⟨n, rfl⟩
  refine ⟨?_, odd_of_val⟩
  rintro ⟨l, rfl⟩
  rw [val_add, val_mul, coe_ofNat_eq_mod, coe_ofNat_eq_mod]
  simp only [Nat.mod_mul_mod, Nat.add_mod_mod, Nat.mod_add_mod, Nat.odd_iff]
  rw [Nat.mod_mod_of_dvd _ ⟨n, (two_mul n).symm⟩, ← Nat.odd_iff, Nat.odd_add_one, Nat.not_odd_iff_even]
  simp

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