Idempotent

📁 Source: Mathlib/Algebra/Group/Idempotent.lean

Statistics

Metric	Count
Definitions IsIdempotentElem, instOneSubtype	2
Theorems coe_one, eq, iff_eq_one, iff_eq_one_of_isUnit, map, mul, mul_mul_self, mul_of_commute, mul_self_mul, of_isIdempotent, one, pow, pow_eq, pow_succ_eq, isIdempotentElem_iff	15
Total	17

IsIdempotentElem

Definitions

Name	Category	Theorems
instOneSubtype 📖	CompOp	3 math math: one_compl, zero_compl, coe_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_one 📖	mathematical	—	IsIdempotentElem MulOne.toMul MulOneClass.toMulOne instOneSubtype MulOne.toOne	—	—
eq 📖	—	IsIdempotentElem	—	—	—
iff_eq_one 📖	mathematical	—	IsIdempotentElem MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid CancelMonoid.toRightCancelMonoid MulOne.toOne	—	LeftCancelSemigroup.toIsLeftCancelMul
iff_eq_one_of_isUnit 📖	mathematical	IsUnit	IsIdempotentElem MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulOne.toOne	—	IsUnit.exists_left_inv eq mul_assoc one_mul one
map 📖	mathematical	IsIdempotentElem	IsIdempotentElem DFunLike.coe	—	eq_1 map_mul eq
mul 📖	mathematical	IsIdempotentElem CommMagma.toMul CommSemigroup.toCommMagma	IsIdempotentElem CommMagma.toMul CommSemigroup.toCommMagma	—	mul_of_commute Commute.all
mul_mul_self 📖	mathematical	IsIdempotentElem Semigroup.toMul	Semigroup.toMul	—	eq mul_assoc
mul_of_commute 📖	mathematical	Commute Semigroup.toMul IsIdempotentElem	IsIdempotentElem Semigroup.toMul	—	eq_1 Commute.mul_mul_mul_comm Commute.symm eq
mul_self_mul 📖	mathematical	IsIdempotentElem Semigroup.toMul	Semigroup.toMul	—	eq mul_assoc
of_isIdempotent 📖	mathematical	—	IsIdempotentElem	—	—
one 📖	mathematical	—	IsIdempotentElem MulOne.toMul MulOneClass.toMulOne MulOne.toOne	—	mul_one
pow 📖	mathematical	IsIdempotentElem MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	IsIdempotentElem MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Monoid.toPow	—	one pow_zero eq sq pow_mul pow_mul'
pow_eq 📖	mathematical	IsIdempotentElem MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toPow	—	pow_succ_eq
pow_succ_eq 📖	mathematical	IsIdempotentElem MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	Monoid.toPow	—	pow_one pow_succ eq

(root)

Definitions

Name	Category	Theorems
IsIdempotentElem 📖	MathDef	102 math math: IsIdempotentElem.star_iff, exists_isIdempotentElem_eq_of_ker_isNilpotent, Matrix.hadamard_self_eq_self_iff, CompleteOrthogonalIdempotents.pair_iff, IsIdempotentElem.coe_compl, IsIdempotentElem.add_sub_mul, InnerProductSpace.isIdempotentElem_rankOne_self, IsIdempotentElem.one_sub, IsIdempotentElem.add, IsIdempotentElem.of_mul_add, OrthogonalIdempotents.isIdempotentElem_sum, PrimeSpectrum.basicOpen_injOn_isIdempotentElem, IsStarProjection.isIdempotentElem, IsIdempotentElem.zero, exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux, Unitization.isIdempotentElem_inr_iff, IsIdempotentElem.one_compl, ContinuousLinearMap.IsIdempotentElem.toLinearMap, IsIdempotentElem.one, Ideal.isIdempotentElem_iff_eq_bot_or_top, LinearMap.isIdempotentElem_iff_eq_isCompl_projection_range_ker, LinearMap.IsSymmetricProjection.isIdempotentElem, LinearMap.isIdempotentElem_map_one_iff, Ideal.isIdempotentElem_iff_of_fg, PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot, PrimeSpectrum.isIdempotentElemEquivClopens_one_sub, Submodule.isIdempotentElem_starProjection, Subalgebra.isIdempotentElem_toSubmodule, orthogonalIdempotents_iff, IsIdempotentElem.iff_eq_one_of_isUnit, IsIdempotentElem.zero_compl, PrimeSpectrum.isClopen_iff, PrimeSpectrum.isIdempotentElemEquivClopens_symm_inf, OrthogonalIdempotents.idem, IsSemisimpleRing.ideal_eq_span_idempotent, ContinuousLinearMap.isIdempotentElem_toLinearMap_iff, Algebra.FormallySmooth.iff_of_surjective, IsIdempotentElem.iff_eq_zero_or_one, AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective, existsUnique_isIdempotentElem_eq_of_ker_isNilpotent, isStarProjection_iff, IsIdempotentElem.of_isIdempotent, isIdempotentElem_one_sub_one_sub_pow_pow, IsIdempotentElem.add_sub_mul_of_commute, IsStarProjection.le_tfae, Submodule.isIdempotentElemEquiv_apply_coe, PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup, isIdempotentElem_iff_quasispectrum_subset, IsIdempotentElem.mul_of_commute, PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen, LinearMap.isIdempotentElem_apply_one_iff, IsIdempotentElem.mul, Algebra.FormallyEtale.Algebra.FormallyEtale.iff_of_surjective, isIdempotentElem_iff_spectrum_subset, Submodule.isIdempotentElemEquiv_symm_apply_coe, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, isIdempotentElem_iff_one_sub_mul_self, LinearMap.IsProj.isIdempotentElem, Unitization.IsIdempotentElem.inr, PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens, PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm, LinearMap.isSymmetricProjection_iff, Ideal.isIdempotentElem_of_pure, IsIdempotentElem.add_iff, IsIdempotentElem.coe_zero, IsIdempotentElem.sub_iff, LinearMap.isProj_range_iff_isIdempotentElem, IsArtinianRing.exists_not_mem_forall_mem_of_ne, IsIdempotentElem.compl_compl, DirectSum.isIdempotentElem_idempotent, ContinuousLinearMap.isStarProjection_iff_isIdempotentElem_and_isStarNormal, BooleanRing.isIdempotentElem, PrimeSpectrum.isIdempotentElemEquivClopens_symm_top, IsLprojection.proj, isStarProjection_iff_isIdempotentElem_and_isStarNormal, IsIdempotentElem.pow, InnerProductSpace.isIdempotentElem_rankOne_self_iff, IsIdempotentElem.star, PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen, PrimeSpectrum.isClopen_iff_zeroLocus, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, IsIdempotentElem.one_sub_iff, IsIdempotentElem.coe_one, Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing, IsIdempotentElem.map, IsMprojection.proj, IsIdempotentElem.iff_eq_one, Algebra.FormallyEtale.iff_of_surjective, isIdempotentElem_iff_mul_one_sub_self, Submodule.IsCompl.projection_isIdempotentElem, isIdempotentElem_iff, PrimeSpectrum.isIdempotentElemEquivClopens_mul, PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply, PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl, LinearMap.toSpanSingleton_isIdempotentElem_iff, isIdempotentElem_star_mul_self_iff_isIdempotentElem_self_mul_star, OrthogonalIdempotents.unique, IsStarProjection.le_iff_idempotent_sub, exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent, IsIdempotentElem.sub, LinearMap.isProj_iff_isIdempotentElem, Ideal.cotangent_subsingleton_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIdempotentElem_iff 📖	mathematical	—	IsIdempotentElem	—	—

---

← Back to Index