smul_def' — Mathlib

English

r • (restrictScalars f).obj M from m equals f r • m; i.e., the restricted scalar action matches the action through f.

Русский

r • m в ограниченном скалярами виде равняется f r • m; то есть действие ограниченных скаляров согласуется через f.

LaTeX

$$$ r \cdot (\text{restrictScalars } f).obj M = (f\,r) \cdot m $$$

Lean4

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

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