nsmul

Mathlib.Analysis.Normed.Group.SemiNormedGrp

URI: https://scilib.ai/kg/mathlib#SemiNormedGrp.Hom.nsmul

English

There is a structure of AddMonoidHomClass on the subtype of NormNoninc elements, between carrier sets.

Русский

Существует структура класса гомоморфизмов добавления на подтип NormNoninc между носителями.

LaTeX

$$AddMonoidHomClass { f : Subtype fun f => f.NormNoninc } X.carrier Y.carrier$$

Lean4

instance nsmul {M N : SemiNormedGrp} : SMul ℕ (M ⟶ N) where smul n f := ofHom (n • f.hom)

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

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

Разделы

Аффилиация

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