eq_zero_or_one_of_sq_eq_self

Mathlib.Algebra.GroupWithZero.Defs

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

English

In a CancelMonoidWithZero, if x^2 = x, then x is either 0 or 1.

Русский

В CancelMonoidWithZero, если x^2 = x, то x равно 0 или 1.

LaTeX

$$$x^2 = x \Rightarrow x = 0 \lor x = 1$ in a CancelMonoidWithZero.$$

Lean4

theorem eq_zero_or_one_of_sq_eq_self (hx : x ^ 2 = x) : x = 0 ∨ x = 1 :=
  or_iff_not_imp_left.mpr (mul_left_injective₀ · <| by simpa [sq] using hx)

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

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

Разделы

Аффилиация

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