restrictScalarsEquiv_mk — Mathlib

English

There is a natural linear equivalence between the quotient M / P.restrictScalars S and M / P, viewed as S-modules.

Русский

Существуют естественные линейные эквивалентности между M / P.RestrictScalars(S) и M / P как S-модули.

LaTeX

$$$$ (M / P_{\\text{restrictScalars } S}) \\simeq_S (M / P). $$$$

Lean4

@[simp]
theorem restrictScalarsEquiv_mk [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) (x : M) :
    restrictScalarsEquiv S P (mk x) = mk x :=
  rfl

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