isCentralScalar — Mathlib

English

If α acts centrally on β, then the induced action of α on Filter β is central; i.e., for every a ∈ α and F ∈ Filter β, a • F = F • a.

Русский

Если α действует как центральный скаляр на β, то индуцированное действие α на Filter β также центрально; то есть для любого a ∈ α и F ∈ Filter β верно a • F = F • a.

LaTeX

$$$\\text{IsCentralScalar}(\\alpha, \\mathrm{Filter}(\\beta)).$$$

Lean4

@[to_additive]
instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsCentralScalar α (Filter β) :=
  ⟨fun _ f => (congr_arg fun m => map m f) <| funext fun _ => op_smul_eq_smul _ _⟩

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