mul_one_sub_self

Mathlib.Algebra.Star.StarProjection

URI: https://scilib.ai/kg/mathlib#IsStarProjection.mul_one_sub_self

English

For a star p, p · (1 − p) = 0.

Русский

Для звездной проекции p выполняется p · (1 − p) = 0.

LaTeX

$$$ p \cdot (1 - p) = 0 $$$

Lean4

theorem mul_one_sub_self [Star R] (hp : IsStarProjection p) : p * (1 - p) = 0 :=
  hp.isIdempotentElem.mul_one_sub_self

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

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

Разделы

Аффилиация

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