addCommGroupFiber

Mathlib.Topology.VectorBundle.Basic

URI: https://scilib.ai/kg/mathlib#VectorBundleCore.addCommGroupFiber

English

The fiber Z.Fiber x naturally carries a commutative additive group structure, compatible with the base field R.

Русский

Фибра Z.Fiber x естественным образом несёт коммутативную аддитивную группу, совместимую с полем R.

LaTeX

$$$\forall x,\; Z.Fiber x \text{ is an AddCommGroup}$$$

Lean4

instance addCommGroupFiber (x : B) : AddCommGroup (Z.Fiber x) :=
  inferInstanceAs (AddCommGroup F)

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

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

Разделы

Аффилиация

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