isCentralScalar — Mathlib

English

If α acts on β and αᵐᵒᵖ acts on β in a central way, then the induced action on Set β makes α central as well.

Русский

Если α действует на β, и αᵐᵒᵖ действует на β в центральном виде, то индуцированное действие на Set β также делает α центральным.

LaTeX

$$$ IsCentralScalar α (Set β) $$$

Lean4

@[to_additive]
instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsCentralScalar α (Set β) :=
  ⟨fun _ S ↦ (congr_arg fun f ↦ f '' S) <| funext fun _ ↦ op_smul_eq_smul _ _⟩

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