The center of a group with zero

def Subgroup.centerUnitsEquivUnitsCenter (G₀ : Type u_1) [GroupWithZero G₀] : ↥(center G₀ˣ) ≃* (↥(Submonoid.center G₀))ˣ

For a group with zero, the center of the units is the same as the units of the center.

@[simp]

theorem Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe (G₀ : Type u_1) [GroupWithZero G₀] (u : (↥(Submonoid.center G₀))ˣ) : ↑↑((centerUnitsEquivUnitsCenter G₀).symm u) = ↑↑u

@[simp]

theorem Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe (G₀ : Type u_1) [GroupWithZero G₀] (a : ↥(center G₀ˣ)) : ↑↑((centerUnitsEquivUnitsCenter G₀) a) = ↑↑a