Commit 2025-01-15 07:14 dc5b3f0c

View on Github →

chore(Idempotent): split into Group, GroupWithZero and Ring parts (#20742) Split Algebra.Idempotents into Algebra.Group.Idempotent, Algebra.GroupWithZero.Idempotent, Algebra.Ring.Idempotent. Rename Order.Idempotents to Algebra.Order.Ring.Idempotent.

Estimated changes

added theorem IsIdempotentElem.eq
added theorem IsIdempotentElem.map
added theorem IsIdempotentElem.mul
added theorem IsIdempotentElem.one
added theorem IsIdempotentElem.pow
added def IsIdempotentElem
added theorem IsIdempotentElem.zero
deleted theorem IsIdempotentElem.coe_one
deleted theorem IsIdempotentElem.coe_zero
deleted theorem IsIdempotentElem.eq
deleted theorem IsIdempotentElem.map
deleted theorem IsIdempotentElem.mul
deleted theorem IsIdempotentElem.one
deleted theorem IsIdempotentElem.one_sub
deleted theorem IsIdempotentElem.pow
deleted theorem IsIdempotentElem.zero
deleted def IsIdempotentElem