instModule_right — Mathlib

English

If R' is a semiring and there is a module structure of R on R', then WithAbs v is an R-module.

Русский

Если R' является полупрямым полумножением и существует структура модуля R на R', то WithAbs v является модулем над R.

LaTeX

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

Lean4

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

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