Theorem isIdempotentElem_iff_one_sub_mul_self

Modification history

2025-06-28 23:20
Mathlib/Algebra/Ring/Idempotent.lean
feat(Algebra/Star/StarProjection): define star projections (#26052) …
Added isIdempotentElem_iff_one_sub_mul_selfView on Github →