Theorems · Theorem · group theory
IsIdempotentElem.map
∀ {M : Type u_4} {N : Type u_5} {F : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
[MulHomClass F M N] {e : M}, IsIdempotentElem e → ∀ (f : F), IsIdempotentElem (f e)- Defined in
- Mathlib.Algebra.Group.Idempotent
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- MulMulFunLikeMulHomClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- FunLikestatement and proof · cited by 2,560
- map_mulproof · cited by 1,137
- IsIdempotentElemstatement and proof · cited by 217
- MulHomClassstatement and proof · cited by 73
- IsIdempotentElem.eqproof · cited by 42
Cited by5
Results whose statement or proof uses this declaration.
- Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_topproof · cited by 1
- Algebra.exists_etale_isIdempotentElem_forall_liesOver_eqproof · cited by 1
- Algebra.FormallyUnramified.pi_iffproof · cited by 1
- Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_auxproof · cited by 1
- IsStarProjection.mapproof · cited by 0