Documentation Verification Report

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`	14
Total	16

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`	`DFunLike.coe`	—	`eq_1` `map_mul` `eq`
`mul` 📖	—	`IsIdempotentElem` `CommMagma.toMul` `CommSemigroup.toCommMagma`	—	—	`mul_of_commute` `Commute.all`
`mul_mul_self` 📖	—	`IsIdempotentElem` `Semigroup.toMul`	—	—	`eq` `mul_assoc`
`mul_of_commute` 📖	—	`Commute` `Semigroup.toMul` `IsIdempotentElem`	—	—	`eq_1` `Commute.mul_mul_mul_comm` `Commute.symm` `eq`
`mul_self_mul` 📖	—	`IsIdempotentElem` `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`	`Monoid.toNatPow`	—	`one` `pow_zero` `eq` `sq` `pow_mul` `pow_mul'`
`pow_eq` 📖	mathematical	`IsIdempotentElem` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`pow_succ_eq`
`pow_succ_eq` 📖	mathematical	`IsIdempotentElem` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Monoid.toNatPow`	—	`pow_one` `pow_succ` `eq`

(root)

Definitions

Name	Category	Theorems
`IsIdempotentElem` 📖	MathDef	75 math math: `IsIdempotentElem.star_iff`, `Matrix.hadamard_self_eq_self_iff`, `CompleteOrthogonalIdempotents.pair_iff`, `IsIdempotentElem.coe_compl`, `InnerProductSpace.isIdempotentElem_rankOne_self`, `IsIdempotentElem.of_mul_add`, `OrthogonalIdempotents.isIdempotentElem_sum`, `PrimeSpectrum.basicOpen_injOn_isIdempotentElem`, `IsStarProjection.isIdempotentElem`, `IsIdempotentElem.zero`, `Unitization.isIdempotentElem_inr_iff`, `IsIdempotentElem.one_compl`, `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`, `isStarProjection_iff`, `IsIdempotentElem.of_isIdempotent`, `isIdempotentElem_one_sub_one_sub_pow_pow`, `Submodule.isIdempotentElemEquiv_apply_coe`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup`, `PrimeSpectrum.exists_idempotent_basicOpen_eq_of_isClopen`, `LinearMap.isIdempotentElem_apply_one_iff`, `Algebra.FormallyEtale.Algebra.FormallyEtale.iff_of_surjective`, `Submodule.isIdempotentElemEquiv_symm_apply_coe`, `isIdempotentElem_iff_one_sub_mul_self`, `LinearMap.IsProj.isIdempotentElem`, `PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens`, `PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm`, `LinearMap.isSymmetricProjection_iff`, `IsIdempotentElem.coe_zero`, `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`, `InnerProductSpace.isIdempotentElem_rankOne_self_iff`, `PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen`, `PrimeSpectrum.isClopen_iff_zeroLocus`, `IsIdempotentElem.one_sub_iff`, `IsIdempotentElem.coe_one`, `Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing`, `IsMprojection.proj`, `IsIdempotentElem.iff_eq_one`, `Algebra.FormallyEtale.iff_of_surjective`, `isIdempotentElem_iff_mul_one_sub_self`, `Submodule.IsCompl.projection_isIdempotentElem`, `PrimeSpectrum.isIdempotentElemEquivClopens_mul`, `PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply`, `PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl`, `LinearMap.toSpanSingleton_isIdempotentElem_iff`, `OrthogonalIdempotents.unique`, `LinearMap.isProj_iff_isIdempotentElem`, `Ideal.cotangent_subsingleton_iff`

---

← Back to Index