origModule — Mathlib

English

The restriction of scalars of a submodule carries an R-module structure inherited from the original submodule.

Русский

Ограничение скаляров подмодуля наследует структуру модуля над R от исходного подмодуля.

LaTeX

$$$$ (p.\\restrictionScalars S) \\\\cong_R p. $$$$

Lean4

/-- Even though `p.restrictScalars S` has type `Submodule S M`, it is still an `R`-module. -/
instance origModule (p : Submodule R M) : Module R (p.restrictScalars S) :=
  (by infer_instance : Module R p)

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