coe_neg

Mathlib.Geometry.Manifold.VectorBundle.SmoothSection

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

English

Define subtraction on ContMDiffSection by pointwise subtraction of fibers.

Русский

Определяем вычитание секций через по точкам вычитание внутри волокон.

LaTeX

$$$\text{instSub}$: $s,t \mapsto s-t$ is a Sub.$$

Lean4

@[simp]
theorem coe_neg (s : Cₛ^n⟮I; F, V⟯) : ⇑(-s : Cₛ^n⟮I; F, V⟯) = -s :=
  rfl

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

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

Разделы

Аффилиация

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