pointwise_isCentralScalar — Mathlib

English

If α acts on M with a central-scalar structure and the action respects the opposite-monoid structure, then the corresponding action on Submonoid M is central as well: IsCentralScalar α (Submonoid M).

Русский

Если α действует на M с центральной скалярной структурой и действие согласовано с противоположным моноидом, то соответствующее действие на Submonoid M тоже центрировано: IsCentralScalar α (Submonoid M).

LaTeX

$$$IsCentralScalar\\;\\alpha\\; (Submonoid\\; M)$$$

Lean4

theorem pointwise_isCentralScalar [MulDistribMulAction αᵐᵒᵖ M] [IsCentralScalar α M] :
    IsCentralScalar α (Submonoid M) :=
  ⟨fun _ S => (congr_arg fun f : Monoid.End M => S.map f) <| MonoidHom.ext <| op_smul_eq_smul _⟩

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