compl_compl — Mathlib

English

On a ring (not necessarily associative), the complement operation on idempotent elements is an involution: applying complement twice returns the original element.

Русский

На кольце (не обязательно ассоциативном) комплемент идемпотентного элемента является инволюцией: двойное применение комплемента возвращает исходный элемент.

LaTeX

$$$a^{\complement\complement} = a$, where $a \in {a : R \mid IsIdempotentElem(a)}$.$$

Lean4

@[simp]
theorem compl_compl (a : { a : R // IsIdempotentElem a }) : aᶜᶜ = a := by ext; simp

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