of_isUnit_two

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#Odd.of_isUnit_two

English

If 2 is a unit, then every element a is odd.

Русский

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

LaTeX

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

Lean4

theorem of_isUnit_two (h : IsUnit (2 : α)) (a : α) : Odd a :=
  by
  rw [← sub_add_cancel a 1]
  exact (Even.of_isUnit_two h _).add_one

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

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

Разделы

Аффилиация

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