leftModule — Mathlib

English

The set I, viewed as a subset of R, carries a natural structure of a left R-module via r · x = r x.

Русский

Множество I, рассматриваемое как подмножество R, обладает естественной структурой левого R-модуля: $r \\cdot x = r x$.

LaTeX

$$$I \\text{ is a left } R\\text{-module with } (r,x) \\mapsto r x$$$

Lean4

instance leftModule : Module R I :=
  Function.Injective.module _ (coeAddMonoidHom I) Subtype.coe_injective fun _ _ ↦ rfl

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