isUnit_two_iff_forall_even — Mathlib

English

In a semiring α, IsUnit(2) holds iff every element is Even.

Русский

В полупрямом кольце α 2 является единицей тогда и только тогда, когда каждый элемент чётен.

LaTeX

$$$IsUnit(2) \iff \forall a,\ \, \operatorname{Even}(a)$$$

Lean4

theorem isUnit_two_iff_forall_even : IsUnit (2 : α) ↔ ∀ a : α, Even a :=
  by
  refine ⟨Even.of_isUnit_two, fun h => ?_⟩
  obtain ⟨a, ha⟩ := h 1
  rw [← two_mul, eq_comm] at ha
  exact ⟨⟨2, a, ha, .trans (Commute.ofNat_right _ _).eq ha⟩, rfl⟩

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