center_units_eq — Mathlib

English

In a group with zero, the center of the unit group equals the preimage of the center under the valuation map: center(Units(G)) = val^{-1}(center(G)).

Русский

В группе с нулём центр группы единиц равен предобразованию центра по отображению Units в G.

LaTeX

$$$center(Units(G_0)) = (\uparrow)^{-1}(center(G_0))$$$

Lean4

/-- In a group with zero, the center of the units is the preimage of the center. -/
theorem center_units_eq : center G₀ˣ = ((↑) : G₀ˣ → G₀) ⁻¹' center G₀ :=
  center_units_subset.antisymm subset_center_units

Похожие утверждения