subset_center_units — Mathlib

English

The preimage of the center under the val map from units to M is contained in the center of the units.

Русский

Обратная проекция центра по отображению значений из единиц в M содержится в центре единиц.

LaTeX

$$$ \text{preimage}(\mathrm{val}, \mathrm{center}(M)) \subseteq \mathrm{center}(\text{Units}(M)) $$$

Lean4

@[to_additive subset_addCenter_add_units]
theorem subset_center_units : ((↑) : Mˣ → M) ⁻¹' center M ⊆ Set.center Mˣ := fun _ ha =>
  by
  rw [_root_.Semigroup.mem_center_iff]
  intro _
  rw [← Units.val_inj, Units.val_mul, Units.val_mul, ha.comm]

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