pointwise_central_scalar — Mathlib

English

If M acts centrally on R, then the induced action of M on Subsemiring R also has a central-scalar structure.

Русский

Если M действует централизованно на R, то полученное действие M на Subsemiring R также имеет структуру центрального скаляра.

LaTeX

$$$IsCentralScalar\,M\,(Subsemiring\,R)$$$

Lean4

instance pointwise_central_scalar [MulSemiringAction Mᵐᵒᵖ R] [IsCentralScalar M R] :
    IsCentralScalar M (Subsemiring R) :=
  ⟨fun _a S => (congr_arg fun f => S.map f) <| RingHom.ext <| op_smul_eq_smul _⟩

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