vadd_def

Mathlib.Algebra.Module.Submodule.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.vadd_def

English

For g in p and m in α, the VAdd on p coincides with the ambient VAdd on M under the inclusion g ↪ g.

Русский

Для элемента g ∈ p и элементов m ∈ α операция VAdd на p совпадает с операцией VAdd в M через вложение g.

LaTeX

$$$g +_V m = (g : M) +_V m$$$

Lean4

theorem vadd_def [VAdd M α] (g : p) (m : α) : g +ᵥ m = (g : M) +ᵥ m :=
  rfl

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

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

Разделы

Аффилиация

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