Idempotents

📁 Source: Mathlib/RingTheory/Idempotents.lean

Statistics

Metric	Count
Definitions `prodQuotientOfIsIdempotentElem`, `CompleteOrthogonalIdempotents`, `ringEquivOfComm`, `ringEquivOfIsMulCentral`, `Corner`, `corner`, `corner`, `OrthogonalIdempotents`, `corner`, `instCommRingCorner`, `instCommSemiringCorner`, `instRingCorner`, `instSemiringCorner`	13
Theorems `prodQuotientOfIsIdempotentElem_apply`, `prodQuotientOfIsIdempotentElem_apply_fst`, `prodQuotientOfIsIdempotentElem_apply_snd`, `bijective_pi`, `bijective_pi'`, `complete`, `equiv`, `iff_ortho_complete`, `lift_of_isNilpotent_ker`, `lift_of_isNilpotent_ker_aux`, `map`, `map_injective_iff`, `of_isIdempotentElem`, `of_ker_isNilpotent`, `of_ker_isNilpotent_of_isMulCentral`, `of_prod_one_sub`, `of_subsingleton`, `option`, `pair_iff`, `pair_iff'ₛ`, `pair_iffₛ`, `prod_one_sub`, `single`, `toOrthogonalIdempotents`, `unique_iff`, `embedding`, `equiv`, `idem`, `iff_mul_eq`, `isIdempotentElem_sum`, `lift_of_isNilpotent_ker`, `lift_of_isNilpotent_ker_aux`, `map`, `map_injective_iff`, `mul_eq`, `mul_sum_of_mem`, `mul_sum_of_notMem`, `option`, `ortho`, `prod_one_sub`, `surjective_pi`, `unique`, `pi_bijective_of_isIdempotentElem`, `prod_bijective_of_isIdempotentElem`, `mem_corner_iff`, `mem_corner_iff_mem_range_mul_left`, `mem_corner_iff_mem_range_mul_right`, `mem_corner_iff_mul_left`, `mem_corner_iff_mul_right`, `completeOrthogonalIdempotents_iff`, `eq_of_isNilpotent_sub_of_isIdempotentElem`, `eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute`, `existsUnique_isIdempotentElem_eq_of_ker_isNilpotent`, `exists_isIdempotentElem_eq_of_ker_isNilpotent`, `exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent`, `exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux`, `isIdempotentElem_one_sub_one_sub_pow_pow`, `orthogonalIdempotents_iff`	58
Total	71

AlgEquiv

Definitions

Name	Category	Theorems
`prodQuotientOfIsIdempotentElem` 📖	CompOp	3 math math: `prodQuotientOfIsIdempotentElem_apply`, `prodQuotientOfIsIdempotentElem_apply_snd`, `prodQuotientOfIsIdempotentElem_apply_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prodQuotientOfIsIdempotentElem_apply` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`DFunLike.coe` `AlgEquiv` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `Prod.instSemiring` `Ideal.Quotient.semiring` `Prod.algebra` `Ideal.instAlgebraQuotient` `instFunLike` `prodQuotientOfIsIdempotentElem` `Ring.toSemiring` `Ideal.instHasQuotient` `RingHom` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `RingHom.instFunLike`	—	—
`prodQuotientOfIsIdempotentElem_apply_fst` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `DFunLike.coe` `AlgEquiv` `Prod.instSemiring` `Ideal.Quotient.semiring` `Prod.algebra` `Ideal.instAlgebraQuotient` `instFunLike` `prodQuotientOfIsIdempotentElem` `RingHom` `Ring.toSemiring` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `RingHom.instFunLike`	—	—
`prodQuotientOfIsIdempotentElem_apply_snd` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.span` `Set` `Set.instSingletonSet` `DFunLike.coe` `AlgEquiv` `Prod.instSemiring` `Ideal.Quotient.semiring` `Prod.algebra` `Ideal.instAlgebraQuotient` `instFunLike` `prodQuotientOfIsIdempotentElem` `RingHom` `Ring.toSemiring` `Ideal.instHasQuotient` `Semiring.toNonAssocSemiring` `Ideal.Quotient.ring` `RingHom.instFunLike`	—	—

CompleteOrthogonalIdempotents

Definitions

Name	Category	Theorems
`ringEquivOfComm` 📖	CompOp	—
`ringEquivOfIsMulCentral` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_pi` 📖	mathematical	`CompleteOrthogonalIdempotents` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `Pi.nonAssocSemiring` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ideal.Quotient.semiring` `RingHom.instFunLike` `Pi.ringHom` `Ideal.instIsTwoSided_1`	—	`Ideal.instIsTwoSided_1` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.induction_on` `one_mul` `mul_assoc` `IsIdempotentElem.eq` `IsIdempotentElem.one_sub` `OrthogonalIdempotents.idem` `toOrthogonalIdempotents` `Finset.prod_insert` `prod_one_sub` `MulZeroClass.zero_mul` `OrthogonalIdempotents.surjective_pi` `Finite.of_fintype`
`bijective_pi'` 📖	mathematical	`CompleteOrthogonalIdempotents` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Pi.nonAssocSemiring` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `Ideal.Quotient.semiring` `RingHom.instFunLike` `Pi.ringHom` `Ideal.instIsTwoSided_1`	—	`Ideal.instIsTwoSided_1` `sub_sub_cancel` `bijective_pi`
`complete` 📖	mathematical	`CompleteOrthogonalIdempotents`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`equiv` 📖	mathematical	—	`CompleteOrthogonalIdempotents` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Finset.sum_congr` `Fintype.sum_equiv`
`iff_ortho_complete` 📖	mathematical	—	`CompleteOrthogonalIdempotents` `Pairwise` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`completeOrthogonalIdempotents_iff` `orthogonalIdempotents_iff` `mul_one` `Finset.sum_eq_single` `Finset.mul_sum`
`lift_of_isNilpotent_ker` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `CompleteOrthogonalIdempotents` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`RingHom.instRingHomClass` `lift_of_isNilpotent_ker_aux` `equiv` `Equiv.symm_apply_apply`
`lift_of_isNilpotent_ker_aux` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `CompleteOrthogonalIdempotents` `Fin.fintype` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`RingHom.instRingHomClass` `subsingleton_or_nontrivial` `of_subsingleton` `one_pow` `NeZero.one` `Finset.sum_congr` `Finset.univ_eq_empty` `Fin.isEmpty'` `complete` `OrthogonalIdempotents.lift_of_isNilpotent_ker` `Finite.of_fintype` `toOrthogonalIdempotents` `equiv` `option` `OrthogonalIdempotents.embedding` `map_sub` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Fin.sum_univ_succ` `map_sum` `add_sub_cancel_right` `finSuccEquiv_succ`
`map` 📖	mathematical	`CompleteOrthogonalIdempotents`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`OrthogonalIdempotents.map` `toOrthogonalIdempotents` `Finset.sum_congr` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `complete` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`map_injective_iff` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`CompleteOrthogonalIdempotents`	—	`OrthogonalIdempotents.map_injective_iff` `Finset.sum_congr` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`of_isIdempotentElem` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`CompleteOrthogonalIdempotents` `Ring.toSemiring` `Fin.fintype` `Matrix.vecCons` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Matrix.vecEmpty`	—	`pair_iff`
`of_ker_isNilpotent` 📖	—	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `CompleteOrthogonalIdempotents` `Ring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	—	`RingHom.instRingHomClass` `of_ker_isNilpotent_of_isMulCentral` `Semigroup.mem_center_iff` `mul_comm`
`of_ker_isNilpotent_of_isMulCentral` 📖	—	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsMulCentral` `CompleteOrthogonalIdempotents` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	—	`RingHom.instRingHomClass` `lift_of_isNilpotent_ker` `eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute` `OrthogonalIdempotents.idem` `toOrthogonalIdempotents` `map_sub` `RingHomClass.toAddMonoidHomClass` `IsMulCentral.comm`
`of_prod_one_sub` 📖	mathematical	`OrthogonalIdempotents` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finset.prod` `CommRing.toCommMonoid` `Finset.univ` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`CompleteOrthogonalIdempotents`	—	`sub_eq_zero` `OrthogonalIdempotents.prod_one_sub`
`of_subsingleton` 📖	mathematical	—	`CompleteOrthogonalIdempotents`	—	—
`option` 📖	mathematical	`OrthogonalIdempotents` `Ring.toSemiring`	`CompleteOrthogonalIdempotents` `instFintypeOption` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.univ`	—	`OrthogonalIdempotents.option` `IsIdempotentElem.one_sub` `OrthogonalIdempotents.isIdempotentElem_sum` `sub_mul` `one_mul` `IsIdempotentElem.eq` `sub_self` `mul_sub` `mul_one` `Fintype.sum_option` `sub_add_cancel`
`pair_iff` 📖	mathematical	—	`CompleteOrthogonalIdempotents` `Ring.toSemiring` `Fin.fintype` `Matrix.vecCons` `Matrix.vecEmpty` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`pair_iff'ₛ` `eq_sub_iff_add_eq'` `mul_sub` `mul_one` `sub_mul` `one_mul`
`pair_iff'ₛ` 📖	mathematical	—	`CompleteOrthogonalIdempotents` `Fin.fintype` `Matrix.vecCons` `Matrix.vecEmpty` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Matrix.cons_val_fin_one` `instIsEmptyFalse` `Fin.instNeZeroHAddNatOfNat_mathlib_1` `Fin.sum_univ_two`
`pair_iffₛ` 📖	mathematical	—	`CompleteOrthogonalIdempotents` `CommSemiring.toSemiring` `Fin.fintype` `Matrix.vecCons` `Matrix.vecEmpty` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`pair_iff'ₛ` `mul_comm`
`prod_one_sub` 📖	mathematical	`CompleteOrthogonalIdempotents` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Finset.prod` `CommRing.toCommMonoid` `Finset.univ` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`OrthogonalIdempotents.prod_one_sub` `toOrthogonalIdempotents` `complete` `sub_self`
`single` 📖	mathematical	—	`CompleteOrthogonalIdempotents` `Pi.semiring` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mul_one` `Pi.single_eq_same` `Pi.single_eq_of_ne` `MulZeroClass.mul_zero` `Pi.single_eq_of_ne'` `MulZeroClass.zero_mul` `Finset.univ_sum_single`
`toOrthogonalIdempotents` 📖	mathematical	`CompleteOrthogonalIdempotents`	`OrthogonalIdempotents`	—	—
`unique_iff` 📖	mathematical	—	`CompleteOrthogonalIdempotents` `Unique.instInhabited` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`completeOrthogonalIdempotents_iff` `OrthogonalIdempotents.unique` `Fintype.sum_unique` `IsIdempotentElem.one`

IsIdempotentElem

Definitions

Name	Category	Theorems
`Corner` 📖	CompOp	—

NonUnitalRing

Definitions

Name	Category	Theorems
`corner` 📖	CompOp	—

NonUnitalSubsemiring

Definitions

Name	Category	Theorems
`corner` 📖	CompOp	—

OrthogonalIdempotents

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embedding` 📖	mathematical	`OrthogonalIdempotents`	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`mul_eq` `Function.instEmbeddingLikeEmbedding`
`equiv` 📖	mathematical	—	`OrthogonalIdempotents` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Equiv.forall_congr_left` `Equiv.apply_symm_apply` `EquivLike.toEmbeddingLike`
`idem` 📖	mathematical	`OrthogonalIdempotents`	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`iff_mul_eq` 📖	mathematical	—	`OrthogonalIdempotents` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`mul_eq`
`isIdempotentElem_sum` 📖	mathematical	`OrthogonalIdempotents`	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Finset.mul_sum` `Finset.sum_congr` `Finset.sum_mul` `mul_eq` `Finset.sum_ite_eq'` `Finset.sum_ite_mem` `Finset.inter_self`
`lift_of_isNilpotent_ker` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `OrthogonalIdempotents` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`RingHom.instRingHomClass` `nonempty_fintype` `lift_of_isNilpotent_ker_aux` `embedding` `Equiv.symm_apply_apply`
`lift_of_isNilpotent_ker_aux` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `OrthogonalIdempotents` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`RingHom.instRingHomClass` `embedding` `exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent` `idem` `isIdempotentElem_sum` `map_sum` `RingHomClass.toAddMonoidHomClass` `Finset.sum_congr` `Finset.mul_sum` `mul_eq` `Finset.sum_const_zero` `Finset.sum_mul` `option` `Equiv.surjective` `finSuccEquiv_symm_none` `finSuccEquiv_symm_some` `finSuccEquiv_succ`
`map` 📖	mathematical	`OrthogonalIdempotents`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_eq` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`map_injective_iff` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`OrthogonalIdempotents`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`mul_eq` 📖	mathematical	`OrthogonalIdempotents`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`ortho` `IsIdempotentElem.eq` `idem`
`mul_sum_of_mem` 📖	mathematical	`OrthogonalIdempotents` `Finset` `Finset.instMembership`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Finset.mul_sum` `Finset.sum_congr` `mul_eq` `Finset.sum_ite_eq`
`mul_sum_of_notMem` 📖	mathematical	`OrthogonalIdempotents` `Finset` `Finset.instMembership`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.mul_sum` `Finset.sum_congr` `mul_eq` `Finset.sum_ite_eq`
`option` 📖	—	`OrthogonalIdempotents` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—	`idem` `mul_assoc` `Finset.sum_mul` `Finset.sum_congr` `mul_eq` `Finset.sum_ite_eq'` `MulZeroClass.zero_mul` `Finset.mul_sum` `Finset.sum_ite_eq` `MulZeroClass.mul_zero` `ortho` `Iff.ne`
`ortho` 📖	mathematical	`OrthogonalIdempotents`	`Pairwise` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`prod_one_sub` 📖	mathematical	`OrthogonalIdempotents` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Finset.prod` `CommRing.toCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Finset.cons_induction` `sub_zero` `Finset.prod_cons` `mul_sub` `mul_one` `sub_mul` `one_mul` `mul_sum_of_notMem` `sub_sub` `Finset.sum_cons`
`surjective_pi` 📖	mathematical	`OrthogonalIdempotents` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `Pi.nonAssocSemiring` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ideal.Quotient.semiring` `RingHom.instFunLike` `Pi.ringHom` `Ideal.instIsTwoSided_1`	—	`Ideal.isCoprime_span_singleton_iff` `mul_sub` `mul_one` `one_mul` `ortho` `sub_zero` `sub_add_cancel` `Ideal.instIsTwoSidedIInf` `Ideal.instIsTwoSided_1` `Ideal.quotientInfToPiQuotient_surj` `Ideal.Quotient.mk_surjective`
`unique` 📖	mathematical	—	`OrthogonalIdempotents` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Unique.instInhabited`	—	`Unique.instSubsingleton`

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pi_bijective_of_isIdempotentElem` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finset.prod` `CommRing.toCommMonoid` `Finset.univ`	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Pi.nonAssocSemiring` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `Ideal.Quotient.semiring` `instFunLike` `Pi.ringHom` `Ideal.instIsTwoSided_1`	—	`CompleteOrthogonalIdempotents.bijective_pi'` `CompleteOrthogonalIdempotents.of_prod_one_sub` `IsIdempotentElem.one_sub` `Finset.prod_congr` `sub_sub_cancel`
`prod_bijective_of_isIdempotentElem` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Function.Bijective` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.span` `Set` `Set.instSingletonSet` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Prod.instNonAssocSemiring` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `instFunLike` `prod`	—	`Ideal.instIsTwoSided_1` `Function.Bijective.of_comp_iff'` `Equiv.bijective` `pi_bijective_of_isIdempotentElem` `Fintype.complete` `add_sub_cancel_left` `add_sub_cancel_right` `mul_comm` `Fin.prod_univ_two`

Subsemigroup

Definitions

Name	Category	Theorems
`corner` 📖	CompOp	5 math math: `mem_corner_iff_mem_range_mul_right`, `mem_corner_iff`, `mem_corner_iff_mul_right`, `mem_corner_iff_mul_left`, `mem_corner_iff_mem_range_mul_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_corner_iff` 📖	mathematical	`IsIdempotentElem` `Semigroup.toMul`	`Subsemigroup` `SetLike.instMembership` `instSetLike` `corner`	—	`IsIdempotentElem.eq` `mul_assoc`
`mem_corner_iff_mem_range_mul_left` 📖	mathematical	`IsIdempotentElem` `Semigroup.toMul` `IsMulCentral`	`Subsemigroup` `SetLike.instMembership` `instSetLike` `corner` `Set` `Set.instMembership` `Set.range`	—	`Commute.eq` `IsMulCentral.comm` `IsIdempotentElem.eq`
`mem_corner_iff_mem_range_mul_right` 📖	mathematical	`IsIdempotentElem` `Semigroup.toMul` `IsMulCentral`	`Subsemigroup` `SetLike.instMembership` `instSetLike` `corner` `Set` `Set.instMembership` `Set.range`	—	`mem_corner_iff_mem_range_mul_left` `Commute.eq` `IsMulCentral.comm`
`mem_corner_iff_mul_left` 📖	mathematical	`IsIdempotentElem` `Semigroup.toMul` `IsMulCentral`	`Subsemigroup` `SetLike.instMembership` `instSetLike` `corner`	—	`mem_corner_iff` `IsMulCentral.comm`
`mem_corner_iff_mul_right` 📖	mathematical	`IsIdempotentElem` `Semigroup.toMul` `IsMulCentral`	`Subsemigroup` `SetLike.instMembership` `instSetLike` `corner`	—	`mem_corner_iff_mul_left` `IsMulCentral.comm`

(root)

Definitions

Name	Category	Theorems
`CompleteOrthogonalIdempotents` 📖	CompData	14 math math: `CompleteOrthogonalIdempotents.pair_iff`, `CompleteOrthogonalIdempotents.of_subsingleton`, `CompleteOrthogonalIdempotents.equiv`, `CompleteOrthogonalIdempotents.option`, `CompleteOrthogonalIdempotents.of_prod_one_sub`, `CompleteOrthogonalIdempotents.single`, `completeOrthogonalIdempotents_iff`, `CompleteOrthogonalIdempotents.unique_iff`, `CompleteOrthogonalIdempotents.iff_ortho_complete`, `CompleteOrthogonalIdempotents.of_isIdempotentElem`, `CompleteOrthogonalIdempotents.map_injective_iff`, `CompleteOrthogonalIdempotents.pair_iff'ₛ`, `DirectSum.completeOrthogonalIdempotents_idempotent`, `CompleteOrthogonalIdempotents.pair_iffₛ`
`OrthogonalIdempotents` 📖	CompData	7 math math: `CompleteOrthogonalIdempotents.toOrthogonalIdempotents`, `OrthogonalIdempotents.iff_mul_eq`, `OrthogonalIdempotents.equiv`, `orthogonalIdempotents_iff`, `completeOrthogonalIdempotents_iff`, `OrthogonalIdempotents.map_injective_iff`, `OrthogonalIdempotents.unique`
`instCommRingCorner` 📖	CompOp	—
`instCommSemiringCorner` 📖	CompOp	—
`instRingCorner` 📖	CompOp	—
`instSemiringCorner` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeOrthogonalIdempotents_iff` 📖	mathematical	—	`CompleteOrthogonalIdempotents` `OrthogonalIdempotents` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`eq_of_isNilpotent_sub_of_isIdempotentElem` 📖	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—	`eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute` `Commute.all`
`eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute` 📖	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Commute`	—	—	`pow_succ` `pow_zero` `mul_sub` `one_mul` `sub_mul` `IsIdempotentElem.eq` `Commute.eq` `mul_assoc` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg` `add_zero` `MulZeroClass.mul_zero` `pow_one` `mul_add` `Distrib.leftDistribClass` `mul_one` `add_assoc` `pow_add` `sub_eq_zero` `MulZeroClass.zero_mul` `Nat.instAtLeastTwoHAddOfNat` `two_mul`
`existsUnique_isIdempotentElem_eq_of_ker_isNilpotent` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `CommRing.toRing` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`ExistsUnique` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	—	`RingHom.instRingHomClass` `exists_isIdempotentElem_eq_of_ker_isNilpotent` `eq_of_isNilpotent_sub_of_isIdempotentElem` `RingHom.mem_ker` `map_sub` `RingHomClass.toAddMonoidHomClass` `sub_self`
`exists_isIdempotentElem_eq_of_ker_isNilpotent` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`RingHom.instRingHomClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent` `IsIdempotentElem.zero`
`exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent` 📖	—	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	—	`RingHom.instRingHomClass` `exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux` `IsIdempotentElem.eq_1` `mul_assoc` `mul_sub` `mul_one` `sub_zero` `IsIdempotentElem.eq` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_sub` `RingHomClass.toAddMonoidHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `sub_mul` `one_mul` `MulZeroClass.mul_zero` `sub_self` `MulZeroClass.zero_mul`
`exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux` 📖	—	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	—	`RingHom.instRingHomClass` `subsingleton_or_nontrivial` `map_sub` `RingHomClass.toAddMonoidHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `sub_zero` `sub_mul` `mul_assoc` `IsIdempotentElem.eq` `sub_self` `pow_two` `isIdempotentElem_one_sub_one_sub_pow_pow` `pow_zero` `NeZero.one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_pow` `IsIdempotentElem.pow_succ_eq` `IsIdempotentElem.one_sub` `sub_sub_cancel` `Commute.sub_dvd_pow_sub_pow` `Commute.one_left` `one_pow` `pow_succ` `MulZeroClass.mul_zero`
`isIdempotentElem_one_sub_one_sub_pow_pow` 📖	mathematical	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`pow_two` `mul_one_sub` `sub_sub_cancel` `one_pow` `Commute.mul_geom_sum₂` `Commute.one_left` `Finset.sum_congr` `one_mul` `Commute.mul_pow` `Commute.sub_left` `Commute.sum_right` `Commute.pow_right` `Commute.mul_mul_mul_comm` `Commute.sub_right` `Commute.one_right` `Commute.sum_left` `Commute.pow_left` `sub_eq_zero` `zero_dvd_iff`
`orthogonalIdempotents_iff` 📖	mathematical	—	`OrthogonalIdempotents` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pairwise` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—

---

← Back to Index