coe_neg

Mathlib.Topology.Algebra.Module.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousAlternatingMap.coe_neg

English

For any f, the postulated composition with negation respects the underlying coercion: (−f) coerces to the negation of f.

Русский

Для любого f нулирование композиции сохраняет: (−f) преобразуется в отрицание f.

LaTeX

$$$\text{coe}(-f) = -\text{coe}(f).$$$

Lean4

@[simp]
theorem coe_neg : ⇑(-f) = -f :=
  rfl

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

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

Разделы

Аффилиация

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