Theorems · Theorem · group theory
IsUnit.map
∀ {F : Type u_1} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : Monoid M] [inst_2 : Monoid N]
[MonoidHomClass F M N] (f : F) {x : M}, IsUnit x → IsUnit (f x)- Defined in
- Mathlib.Algebra.Group.Units.Hom
- Cited by
- 104 results in Mathlib
- Foundations
- Depth 25 from the axioms, rests on 174 definitions · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- Monoidstatement and proof · cited by 3,887
- Unitsproof · cited by 2,804
- FunLikestatement and proof · cited by 2,560
- Units.valproof · cited by 1,966
- IsUnitstatement and proof · cited by 1,602
- MonoidHomClass.toMonoidHomproof · cited by 294
- MonoidHomClassstatement and proof · cited by 244
- Units.isUnitproof · cited by 116
- Units.mapproof · cited by 95
Cited by104
Results whose statement or proof uses this declaration.
- Polynomial.isUnit_Cproof · cited by 19
- isUnit_map_iffproof · cited by 17
- RingHom.isUnit_mapproof · cited by 14
- IsLocalization.isLocalization_of_algEquivproof · cited by 11
- IsLocalizedModule.isBaseChangeproof · cited by 9
- Algebra.EssFiniteType.compproof · cited by 7
- IsLocalization.away_of_isUnit_of_bijectiveproof · cited by 6
- Algebra.FormallySmooth.of_isLocalizationproof · cited by 6
- IsLocalization.Away.of_associatedproof · cited by 6
- Algebra.FormallyUnramified.of_isSeparableproof · cited by 5
- Irreducible.of_mapproof · cited by 4
- Submodule.range_unitsToPicproof · cited by 4