Theorems · Theorem · group theory
Submonoid.map_powers
∀ {M : Type u_1} [inst : Monoid M] {N : Type u_4} {F : Type u_5} [inst_1 : Monoid N] [inst_2 : FunLike F M N]
[inst_3 : MonoidHomClass F M N] (f : F) (m : M), Submonoid.map f (Submonoid.powers m) = Submonoid.powers (f m)- Cited by
- 10 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- Setproof · cited by 53,352
- Monoidstatement and proof · cited by 3,887
- Submonoidstatement · cited by 3,086
- FunLikestatement and proof · cited by 2,560
- Submonoid.powersstatement and proof · cited by 408
- MonoidHomClassstatement and proof · cited by 244
- Submonoid.mapstatement · cited by 190
- Set.image_singletonproof · cited by 174
- Submonoid.closureproof · cited by 167
- MonoidHom.map_mclosureproof · cited by 10
- Submonoid.map.congr_simpproof · cited by 9
Cited by10
Results whose statement or proof uses this declaration.
- Algebra.algebraMapSubmonoid_powersproof · cited by 9
- RingHom.LocalizationPreserves.awayproof · cited by 9
- IsLocalization.Away.mapₐ_surjective_of_surjectiveproof · cited by 2
- Algebra.IsStandardEtale.of_isLocalizationAwayproof · cited by 2
- RingHom.locally_localizationAwayPreservesproof · cited by 1
- RingHom.ker_fg_of_localizationSpanproof · cited by 1
- RingHom.locally_respectsIsoproof · cited by 1
- Algebra.FiniteType.of_span_eq_top_sourceproof · cited by 1
- RingHom.locally_localizationPreservesproof · cited by 0
- RingHom.finite_ofLocalizationSpanproof · cited by 0