smul_def — Mathlib

English

Restriction of scalars does not change the action of a morphism on elements; the map is pointwise the same.

Русский

Ограничение скаляров не изменяет действие мономорфизма на элементы; отображение действует по точкам одинаково.

LaTeX

$$$(\mathrm{restrictScalars}(f)).\mathrm{map} g (x) = g(x)$ for all x$$

Lean4

@[simp]
theorem smul_def {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) {M : ModuleCat.{v} S} (r : R)
    (m : (restrictScalars f).obj M) : r • m = f r • show M from m :=
  rfl

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