isCentralScalar — Mathlib

English

If α β with SMul α β and SMul αᵐᵒᵖ β and IsCentralScalar α β, then Finset β has IsCentralScalar α (Finset β).

Русский

Если α действует на β центрально и αᵐᵒᵖ дублирует это действие, то Finset β наследует центральное скалярное действие от α.

LaTeX

$$$IsCentralScalar\ α\ (Finset\ β).$$$

Lean4

@[to_additive]
instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsCentralScalar α (Finset β) :=
  ⟨fun a s => coe_injective <| by simp only [coe_smul_finset, op_smul_eq_smul]⟩

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