Theorems · Theorem · commutative algebra
IsIdempotentElem.one_sub
∀ {R : Type u_1} [inst : NonAssocRing R] {a : R}, IsIdempotentElem a → IsIdempotentElem (1 - a)- Defined in
- Mathlib.Algebra.Ring.Idempotent
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext
- Assumes
- NonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- sub_selfproof · cited by 996
- sub_zeroproof · cited by 938
- NonAssocRingstatement and proof · cited by 483
- IsIdempotentElemstatement and proof · cited by 217
- mul_subproof · cited by 201
- sub_mulproof · cited by 170
- IsIdempotentElem.eqproof · cited by 42
Cited by20
Results whose statement or proof uses this declaration.
- IsLprojection.Lcomplementproof · cited by 3
- LinearMap.IsIdempotentElem.ker_eq_rangeproof · cited by 3
- CompleteOrthogonalIdempotents.bijective_piproof · cited by 2
- IsStarProjection.one_subproof · cited by 2
- Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_isLocalRingproof · cited by 1
- CompleteOrthogonalIdempotents.optionproof · cited by 1
- Algebra.FormallyUnramified.exists_algEquiv_prodproof · cited by 1
- exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_auxproof · cited by 1
- PrimeSpectrum.zeroLocus_eq_basicOpen_of_isIdempotentElemproof · cited by 1
- PrimeSpectrum.isClopen_iff_zeroLocusproof · cited by 1
- Algebra.IsStandardEtale.of_surjectiveproof · cited by 1
- RingHom.pi_bijective_of_isIdempotentElemproof · cited by 1