natCast_eq_zero_or_one_of_two_eq_zero

English

If 2 = 0 in R, then for any n, n cast in R is either 0 or 1, depending on parity of n.

Русский

Если 2 = 0 в R, то для любого n отображение n в R равно либо 0, либо 1, завися от парности n.

LaTeX

$$$\forall n, \left(n : R\right) = 0 \lor \left(n : R\right) = 1.$$$

Lean4

theorem natCast_eq_zero_or_one_of_two_eq_zero (n : ℕ) (h : (2 : R) = 0) : (n : R) = 0 ∨ (n : R) = 1 :=
  by
  obtain hn | hn := Nat.even_or_odd n
  · exact Or.inl <| natCast_eq_zero_of_even_of_two_eq_zero hn h
  · exact Or.inr <| natCast_eq_one_of_odd_of_two_eq_zero hn h

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