Commit 2024-07-25 00:13 5e9604dc

View on Github →

feat(RingTheory/Idempotents): Lifting complete orthogonal idempotents along nil extensions (#14372)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Idempotents.lean

added theorem CompleteOrthogonalIdempotents.bijective_pi'

added theorem CompleteOrthogonalIdempotents.bijective_pi

added theorem CompleteOrthogonalIdempotents.equiv

added theorem CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker

added theorem CompleteOrthogonalIdempotents.lift_of_isNilpotent_ker_aux

added theorem CompleteOrthogonalIdempotents.map

added theorem CompleteOrthogonalIdempotents.map_injective_iff

added theorem CompleteOrthogonalIdempotents.of_isIdempotentElem

added theorem CompleteOrthogonalIdempotents.of_ker_isNilpotent

added theorem CompleteOrthogonalIdempotents.of_ker_isNilpotent_of_isMulCentral

added theorem CompleteOrthogonalIdempotents.of_prod_one_sub

added theorem CompleteOrthogonalIdempotents.of_subsingleton

added theorem CompleteOrthogonalIdempotents.option

added theorem CompleteOrthogonalIdempotents.pair_iff

added theorem CompleteOrthogonalIdempotents.prod_one_sub

added theorem CompleteOrthogonalIdempotents.single

added theorem CompleteOrthogonalIdempotents.unique_iff

added structure CompleteOrthogonalIdempotents

added theorem OrthogonalIdempotents.embedding

added theorem OrthogonalIdempotents.equiv

added theorem OrthogonalIdempotents.iff_mul_eq

added theorem OrthogonalIdempotents.isIdempotentElem_sum

added theorem OrthogonalIdempotents.lift_of_isNilpotent_ker

added theorem OrthogonalIdempotents.lift_of_isNilpotent_ker_aux

added theorem OrthogonalIdempotents.map

added theorem OrthogonalIdempotents.map_injective_iff

added theorem OrthogonalIdempotents.mul_eq

added theorem OrthogonalIdempotents.option

added theorem OrthogonalIdempotents.prod_one_sub

added theorem OrthogonalIdempotents.surjective_pi

added theorem OrthogonalIdempotents.unique

added structure OrthogonalIdempotents

added theorem bijective_pi_of_isIdempotentElem

added theorem eq_of_isNilpotent_sub_of_isIdempotentElem

added theorem eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute

added theorem existsUnique_isIdempotentElem_eq_of_ker_isNilpotent

added theorem exists_isIdempotentElem_eq_of_ker_isNilpotent

added theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent

added theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux

added theorem isIdempotentElem_one_sub_one_sub_pow_pow