restrictScalarsEquiv — Mathlib

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 }

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