Theorems · Definition · group theory
AddUnits.map
{M : Type u} → {N : Type v} → [inst : AddMonoid M] → [inst_1 : AddMonoid N] → (M →+ N) → AddUnits M →+ AddUnits NThe additive homomorphism on AddUnits induced by an AddMonoidHom.
- Defined in
- Mathlib.Algebra.Group.Units.Hom
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 24 from the axioms · 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
- AddMonoidHomstatement and proof · cited by 3,230
- AddMonoidstatement and proof · cited by 2,864
- AddUnitsstatement and proof · cited by 325
- AddUnits.valproof · cited by 248
- AddMonoidHom.mk'proof · cited by 25
- AddUnits.negproof · cited by 14
Cited by18
Results whose statement or proof uses this declaration.
- IsAddUnit.mapproof · cited by 16
- addUnitsCenterToCenterAddUnitsproof · cited by 2
- AddUnits.continuous_mapstatement · cited by 2
- AddEquiv.prodAddUnitsproof · cited by 1
- AddSubmonoid.LocalizationMap.isAddUnit_compproof · cited by 1
- AddUnits.coe_mapstatement · cited by 1
- AddUnits.map_injectivestatement and proof · cited by 1
- IsTopologicalAddGroup.isOpenMap_iff_nhds_zeroproof · cited by 0
- AddUnits.coe_map_negstatement · cited by 0
- AddUnits.isOpenMap_mapstatement and proof · cited by 0
- AddUnits.map_bijectivestatement · cited by 0
- AddUnits.map_compstatement · cited by 0