range_two_mul

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#range_two_mul

English

In a semiring, the even elements are precisely the elements of the form 2x.

Русский

В полугруппе чётные элементы совпадают с элементами вида 2x.

LaTeX

$$$\{2x \mid x \in \alpha\} = \{a \in \alpha \mid \operatorname{Even}(a)\}$$$

Lean4

@[simp]
theorem range_two_mul (α) [NonAssocSemiring α] : Set.range (fun x : α ↦ 2 * x) = {a | Even a} :=
  by
  ext x
  simp [eq_comm, two_mul, Even]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru