center_units_subset — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem center_units_subset : center G₀ˣ ⊆ ((↑) : G₀ˣ → G₀) ⁻¹' center G₀ :=
  by
  simp_rw [subset_def, mem_preimage, _root_.Semigroup.mem_center_iff]
  intro u hu a
  obtain rfl | ha := eq_or_ne a 0
  · rw [zero_mul, mul_zero]
  · exact congr_arg Units.val <| hu <| Units.mk0 a ha

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