English
There is a natural R-linear equivalence between a restricted submodule and the original submodule.
Русский
Существует естественное R-линейное эквивалентное отображение между ограниченным скалярами подмодулом и исходным подмодулем.
LaTeX
$$$$ (p.\\restrictionScalars S) \\simeq_R p. $$$$
Lean4
/-- Turning `p : Submodule R M` into an `S`-submodule gives the same module structure
as turning it into a type and adding a module structure. -/
@[simps +simpRhs]
def restrictScalarsEquiv (p : Submodule R M) : p.restrictScalars S ≃ₗ[R] p :=
{ AddEquiv.refl p with map_smul' := fun _ _ => rfl }