English
The map from units of the center to the center of the units is injective.
Русский
Отображение единиц центра в центр единиц инъективно.
LaTeX
$$injective(unitsCenterToCenterUnits M)$$
Lean4
/-- For a monoid, the units of the center inject into the center of the units. This is not an
equivalence in general; one case where this holds is for groups with zero, which is covered in
`centerUnitsEquivUnitsCenter`. -/
@[to_additive (attr := simps! apply_coe_val) /--
For an additive monoid, the units of the center inject into the center of the units. -/
]
def unitsCenterToCenterUnits [Monoid M] : (Submonoid.center M)ˣ →* Submonoid.center (Mˣ) :=
(Units.map (Submonoid.center M).subtype).codRestrict _ <| fun u ↦
Submonoid.mem_center_iff.mpr <| fun r ↦
Units.ext <| by
rw [Units.val_mul, Units.coe_map, Submonoid.coe_subtype, Units.val_mul, Units.coe_map, Submonoid.coe_subtype,
u.1.prop.comm r]
