instModule_left

Mathlib.Analysis.Normed.Ring.WithAbs

URI: https://scilib.ai/kg/mathlib#WithAbs.instModule_left

English

If R' is an AddCommGroup and a module over R, then WithAbs v is an R'-module.

Русский

Если R' является аддитивной группой и модулем над R, то WithAbs v является модулем над R'.

LaTeX

$$Module_{R'}(WithAbs(v))$$

Lean4

instance instModule_left [AddCommGroup R'] [Module R R'] (v : AbsoluteValue R S) : Module (WithAbs v) R' :=
  inferInstanceAs <| Module R R'

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

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

Разделы

Аффилиация

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