toModule — Mathlib

English

A ring hom f : R →+* S defines a module structure on S over R by r • s = f(r) s.

Русский

Кольцевой гомоморфизм f : R →+* S задаёт структуру модуля S над R через r • s = f(r) s.

LaTeX

$$$r \\cdot s := f(r) s$$$

Lean4

/-- A ring homomorphism `f : R →+* M` defines a module structure by `r • x = f r * x`.
See note [reducible non-instances]. -/
abbrev toModule [Semiring R] [Semiring S] (f : R →+* S) : Module R S :=
  Module.compHom S f

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