Theorems · Definition · group theory
MonoidHom.mrange
{M : Type u_1} →
{N : Type u_2} →
[inst : MulOneClass M] →
[inst_1 : MulOneClass N] →
{F : Type u_4} → [inst_2 : FunLike F M N] → [mc : MonoidHomClass F M N] → F → Submonoid NThe range of a MonoidHom is a Submonoid. See Note [range copy pattern].
- Cited by
- 63 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- DFunLike.coeproof · cited by 62,936
- Top.topproof · cited by 9,680
- Set.rangeproof · cited by 4,705
- Submonoidstatement · cited by 3,086
- FunLikestatement and proof · cited by 2,560
- MulOneClassstatement and proof · cited by 1,018
- MonoidHomClassstatement and proof · cited by 244
- Submonoid.mapproof · cited by 190
- Submonoid.copyproof · cited by 4
Cited by68
Results whose statement or proof uses this declaration.
- Submonoid.powersproof · cited by 408
- MonoidHom.mrange_eq_mapstatement · cited by 13
- MonoidHom.coe_mrangestatement · cited by 6
- MonoidHom.mrange_eq_top_of_surjectivestatement · cited by 6
- MonoidHom.mrangeRestrictstatement and proof · cited by 5
- Submonoid.mrange_subtypestatement and proof · cited by 4
- MonoidHom.mrange_eq_topstatement · cited by 4
- Polynomial.splits_iff_exists_multiset'proof · cited by 4
- Submonoid.closure_eq_mrangestatement · cited by 3
- MonoidHom.exists_mrange_eq_mgraphstatement · cited by 3
- Con.lift_rangestatement and proof · cited by 2
- Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integerstatement and proof · cited by 2