instZero — Mathlib

English

The collection of C^k-sections forms an additive commutative group under pointwise operations.

Русский

Множество C^k-секций образует коммутативную аддитивную группу по точечным операциям.

LaTeX

$$$\mathrm{ContMDiffSection.instAddCommGroup}$ defines an AddCommGroup structure on $C_\s^n(I;F,V)$.$$

Lean4

instance instZero : Zero Cₛ^n⟮I; F, V⟯ :=
  ⟨⟨fun _ => 0, (contMDiff_zeroSection 𝕜 V).of_le le_top⟩⟩

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