Theorems · Definition · group theory
Units.map
{M : Type u} → {N : Type v} → [inst : Monoid M] → [inst_1 : Monoid N] → (M →* N) → Mˣ →* NˣThe group homomorphism on units induced by a MonoidHom.
- Defined in
- Mathlib.Algebra.Group.Units.Hom
- Cited by
- 95 results in Mathlib
- Foundations
- Depth 24 from the axioms, rests on 166 definitions · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement and proof · cited by 3,629
- Unitsstatement and proof · cited by 2,804
- Units.valproof · cited by 1,966
- Units.invproof · cited by 35
- MonoidHom.mk'proof · cited by 3
Cited by131
Results whose statement or proof uses this declaration.
- IsUnit.mapproof · cited by 104
- LinearEquiv.detproof · cited by 51
- Matrix.GeneralLinearGroup.mapproof · cited by 29
- ZMod.unitsMapproof · cited by 24
- ClassGroup.mkproof · cited by 22
- Matrix.GeneralLinearGroup.scalarproof · cited by 18
- Units.mapEquivproof · cited by 16
- MulChar.toUnitHomproof · cited by 14
- WeierstrassCurve.VariableChange.mapproof · cited by 9
- MulChar.domRestrictproof · cited by 8
- MulEquiv.prodUnitsproof · cited by 7
- AffineEquiv.equivUnitsAffineMapproof · cited by 7