Commit 2022-12-09 12:21 a461e549

View on Github →

feat port: Algebra.Ring.Idempotents (#918) 655994e298904d7e5bbd1e18c95defd7b543eb94 No real problems here. One nth_rw changed to a conv_rhs

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/Idempotents.lean

added theorem IsIdempotentElem.coe_compl

added theorem IsIdempotentElem.coe_one

added theorem IsIdempotentElem.coe_zero

added theorem IsIdempotentElem.compl_compl

added theorem IsIdempotentElem.eq

added theorem IsIdempotentElem.iff_eq_one

added theorem IsIdempotentElem.iff_eq_zero_or_one

added theorem IsIdempotentElem.mul_of_commute

added theorem IsIdempotentElem.of_isIdempotent

added theorem IsIdempotentElem.one

added theorem IsIdempotentElem.one_compl

added theorem IsIdempotentElem.one_sub

added theorem IsIdempotentElem.one_sub_iff

added theorem IsIdempotentElem.pow

added theorem IsIdempotentElem.pow_succ_eq

added theorem IsIdempotentElem.zero

added theorem IsIdempotentElem.zero_compl

added def IsIdempotentElem