of_isUnit_two — Mathlib

English

If 2 is a unit in α, then every element a ∈ α is even.

Русский

Если 2 является единицей в кольце α, то любой элемент α является чётным.

LaTeX

$$$\operatorname{IsUnit}(2) \Rightarrow \forall a\in \alpha,\ \operatorname{Even}(a)$$$

Lean4

theorem of_isUnit_two (h : IsUnit (2 : α)) (a : α) : Even a :=
  let ⟨u, hu⟩ := h;
  ⟨u⁻¹ * a, by rw [← mul_add, ← two_mul, ← hu, Units.inv_mul_cancel_left]⟩

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