instInhabited

Mathlib.LinearAlgebra.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#AlternatingMap.instInhabited

English

Addition on alternating maps is defined pointwise: (f + g)(v) = f(v) + g(v).

Русский

Сложение чередующихся отображений определено покоординатно: (f + g)(v) = f(v) + g(v).

LaTeX

$$$ (f + g)(v) = f(v) + g(v). $$$

Lean4

instance instInhabited : Inhabited (M [⋀^ι]→ₗ[R] N) :=
  ⟨0⟩

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

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

Разделы

Аффилиация

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