instIsCancelAdd

Mathlib.Algebra.Group.Finsupp

URI: https://scilib.ai/kg/mathlib#Finsupp.instIsCancelAdd

English

Given M and N with IsCancelAdd, the finsupp space ι →₀ M inherits the cancel-add property.

Русский

При IsCancelAdd для M и N пространство ι →₀ M наследует свойство отмены сложения.

LaTeX

$$$\\text{IsCancelAdd}(M) \\Rightarrow \\text{IsCancelAdd}(\\iota \\to_{0} M)$$$

Lean4

instance instIsCancelAdd [IsCancelAdd M] : IsCancelAdd (ι →₀ M) where

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

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

Разделы

Аффилиация

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