restrictScalars_toSubmodule — Mathlib

English

The R-submodule associated to restrictScalars(R,U) coincides with the restricted submodule of U.

Русский

Связанный с ограничением скаляра по R-подмодуль совпадает с ограниченным подмодулем U.

LaTeX

$$$\operatorname{toSubmodule}(\restrictScalars R U) = U^{\uparrow R}$$$

Lean4

@[simp]
theorem restrictScalars_toSubmodule {U : Subalgebra S A} :
    Subalgebra.toSubmodule (U.restrictScalars R) = U.toSubmodule.restrictScalars R :=
  SetLike.coe_injective rfl

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