instModuleQuotientIdealSpanSingletonSetSubtypeMemTorsionBy

English

For a commutative ring R and an R-module M, the a-torsion submodule torsionBy(R, M, a) carries a natural module structure over the quotient ring R/Ideal.span{a}.

Русский

Для кольца R и R-модуля M подмодуль a-тродировки torsionBy(R, M, a) естественным образом является модулем над кольцом-кватентом R/Ideal.span{a}.

LaTeX

$$$\\operatorname{torsionBy}(R,M,a)$ is a module over $R/\\operatorname{Ideal.span}\\{a\\}$.$$

Lean4

instance (a : R) : Module (R ⧸ Ideal.span { a }) (torsionBy R M a) :=
  inferInstanceAs <| Module (R ⧸ R ∙ a) (torsionBy R M a)

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