units_val — Mathlib

English

If two units u1 and u2 commute in the units group, then their underlying elements in M commute: Commute u1 u2 → Commute (u1 : M) u2.

Русский

Если две единицы u1 и u2 коммутируют как элементы группы единиц, тогда их числовые значения в M также коммутируют.

LaTeX

$$Commute u1 u2 \Rightarrow Commute (u1 : M) u2$$

Lean4

@[to_additive]
theorem units_val : Commute u₁ u₂ → Commute (u₁ : M) u₂ :=
  SemiconjBy.units_val

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