Theorem IsIdempotentElem.mul

Modification history

2025-01-15 07:14

Mathlib/Algebra/Group/Idempotent.lean

chore(Idempotent): split into `Group`, `GroupWithZero` and `Ring` parts (#20742) …

Modified IsIdempotentElem.mul View on Github →

2024-10-03 17:44

Mathlib/Algebra/Ring/Idempotents.lean

feat(RingTheory/Unramified): Formally unramified product of rings (#15141)

Added IsIdempotentElem.mul View on Github →