instHasDistribNegSubtypeMemSubmonoid

Mathlib.Algebra.Star.Unitary

URI: https://scilib.ai/kg/mathlib#unitary.instHasDistribNegSubtypeMemSubmonoid

English

The subtype of unitary elements inherits the distributive neg property: for x,y in the subtype, -(xy) = (-x)y.

Русский

Подтип унитарных элементов наследует свойство распределения отрицания: для x,y в подтипе -(xy) = (-x)y.

LaTeX

$$$-(xy) = (-x)\,y$$$

Lean4

instance : HasDistribNeg (unitary R) :=
  Subtype.coe_injective.hasDistribNeg _ coe_neg (unitary R).coe_mul

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

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

Разделы

Аффилиация

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