instHasDistribNeg

Mathlib.Analysis.Complex.UnitDisc.Basic

URI: https://scilib.ai/kg/mathlib#Complex.UnitDisc.instHasDistribNeg

English

Negation distributes over addition in the unit disk: -(z1+z2) = (-z1) + (-z2).

Русский

Отрицание распределено по сложению в единичном диске: -(z1+z2) = (-z1) + (-z2).

LaTeX

$$$-(z_1 + z_2) = (-z_1) + (-z_2)$$$

Lean4

instance instHasDistribNeg : HasDistribNeg UnitDisc := by unfold UnitDisc; infer_instance

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

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

Разделы

Аффилиация

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