Documentation

Mathlib.Algebra.GroupWithZero.Action.Center

The center of a group with zero #

source
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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe (G₀ : Type u_1) [GroupWithZero G₀] (u : (↥(Submonoid.center G₀))ˣ) :
    ↑↑((centerUnitsEquivUnitsCenter G₀).symm u) = ↑↑u
    source
    @[simp]
    theorem Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe (G₀ : Type u_1) [GroupWithZero G₀] (a : ↥(center G₀ˣ)) :
    ↑↑((centerUnitsEquivUnitsCenter G₀) a) = ↑↑a