pointwise_isCentralScalar — Mathlib

English

If M acts centrally on A and there is a central scalar, then M acts centrally on AddSubmonoid A.

Русский

Если M действует централизованно на A и имеется центральный скаляр, то M действует централизованно на AddSubmonoid A.

LaTeX

$$$ IsCentralScalar M (AddSubmonoid A) $$$

Lean4

theorem pointwise_isCentralScalar [DistribMulAction Mᵐᵒᵖ A] [IsCentralScalar M A] :
    IsCentralScalar M (AddSubmonoid A) :=
  ⟨fun _ S => (congr_arg fun f : AddMonoid.End A => S.map f) <| AddMonoidHom.ext <| op_smul_eq_smul _⟩

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