coe_neg'

Mathlib.Topology.Algebra.Module.LinearMap

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.coe_neg'

English

The coercion of -f equals the additive negation of f as a linear map.

Русский

Приведение -f к линейному отображению равно плюс-минусому отображению f.

LaTeX

$$⇑(-f) = -f$$

Lean4

@[norm_cast]
theorem coe_neg' (f : M →SL[σ₁₂] M₂) : ⇑(-f) = -f :=
  rfl

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

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

Разделы

Аффилиация

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