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