English
If a is idempotent in a monoid (a^2 = a), then the submonoid generated by a contains only the two elements 1 and a; equivalently, the set of powers of a is {1, a}.
Русский
Если a идемпотентен в моноиде (a^2 = a), порожденный a подмножество содержит только элементы 1 и a; множество степеней a равно {1, a}.
LaTeX
$$$ (\\operatorname{powers}(a) : Set M) = \\{1, a\\} $$$
Lean4
theorem _root_.IsIdempotentElem.coe_powers {a : M} (ha : IsIdempotentElem a) :
(Submonoid.powers a : Set M) = { 1, a } :=
let S : Submonoid M :=
{ carrier := { 1, a },
mul_mem' := by
rintro _ _ (rfl | rfl) (rfl | rfl)
· rw [one_mul]; exact .inl rfl
· rw [one_mul]; exact .inr rfl
· rw [mul_one]; exact .inr rfl
· rw [ha]; exact .inr rfl
one_mem' := .inl rfl }
suffices Submonoid.powers a = S from congr_arg _ this
le_antisymm (Submonoid.powers_le.mpr <| .inr rfl)
(by rintro _ (rfl | rfl); exacts [one_mem _, Submonoid.mem_powers _])
