Theorem IsIdempotentElem.mul_eq_zero_of_anticommute

Modification history

2026-09-30 14:37
Mathlib/Algebra/Ring/Idempotent.lean
refactor(Algebra/Group): fix the definition of torsion-free non-abelian groups (#42407) …
Modified IsIdempotentElem.mul_eq_zero_of_anticommuteView on Github →
2025-06-28 23:20
Mathlib/Algebra/Ring/Idempotent.lean
feat(Algebra/Star/StarProjection): define star projections (#26052) …
Added IsIdempotentElem.mul_eq_zero_of_anticommuteView on Github →