units_of_val

Mathlib.Algebra.Group.Semiconj.Units

URI: https://scilib.ai/kg/mathlib#SemiconjBy.units_of_val

English

If SemiconjBy (a : M) x y holds, then SemiconjBy a x y holds in Units M.

Русский

Если SemiconjBy (a : M) x y выполняется, то SemiconjBy a x y верно и в группе единиц.

LaTeX

$$$$\forall a,x,y:\ SemiconjBy (a : M) x y \Rightarrow SemiconjBy a x y.$$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru