of_one_ne_zero_of_two_eq_zero — Mathlib

English

If 1 ≠ 0 and 2 = 0 in a ring, then CharP R 2.

Русский

Если 1 ≠ 0 и 2 = 0 в кольце, то CharP R 2.

LaTeX

$$$(1 \neq 0) \land (2 = 0) \Rightarrow \\mathrm{CharP}(R) 2$$$

Lean4

/-- The only hypotheses required to build a `CharP R 2` instance are `1 ≠ 0` and `2 = 0`. -/
theorem of_one_ne_zero_of_two_eq_zero (h₁ : (1 : R) ≠ 0) (h₂ : (2 : R) = 0) : CharP R 2 where
  cast_eq_zero_iff
    n := by
    obtain hn | hn := Nat.even_or_odd n
    · simp_rw [hn.two_dvd, iff_true]
      exact natCast_eq_zero_of_even_of_two_eq_zero hn h₂
    · simp_rw [hn.not_two_dvd_nat, iff_false]
      rwa [natCast_eq_one_of_odd_of_two_eq_zero hn h₂]

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