toSubbimoduleInt — Mathlib

English

Base change from R ⊗[ℤ] S to R ⊗[ℕ] S along the natural numbers yields a Submodule over the latter from the former.

Русский

Базисное изменение по ℕ переводит подмодуль с R ⊗ℤ S на R ⊗ℕ S.

LaTeX

$$$$ toSubbimoduleNat(p) = \\mathrm{baseChange}_{\\mathbb{N}}(p). $$$$

Lean4

/-- A `Submodule` over `R ⊗[ℕ] S` is naturally also a `Submodule` over the canonically-isomorphic
ring `R ⊗[ℤ] S`. -/
@[simps!]
def toSubbimoduleInt (p : Submodule (R ⊗[ℕ] S) M) : Submodule (R ⊗[ℤ] S) M :=
  baseChange ℤ p

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