units_val — Mathlib

English

If SemiconjBy a x y holds for units a,x,y, then SemiconjBy (a: M) x y in M holds as well.

Русский

Если SemiconjBy a x y выполняется для единиц a, x, y, то такое же полусопряжение верно и в самом Monoid.

LaTeX

$$$$\forall a,x,y\in M^{\times}:\ SemiconjBy a x y \implies SemiconjBy (a: M) x y.$$$$

Lean4

@[to_additive]
theorem units_val {a x y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy (a : M) x y :=
  congr_arg Units.val h

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