instIsCentralScalar — Mathlib

English

There is an IsCentralScalar structure on c.Quotient, making the scalar action central with respect to the base monoid.

Русский

На фактор-модуля c.Quotient существует структура IsCentralScalar, обеспечивающая центральность скалярного действия.

LaTeX

$$IsCentralScalar α c.Quotient$$

Lean4

instance instIsCentralScalar {α M : Type*} [MulOneClass M] [SMul α M] [SMul αᵐᵒᵖ M] [IsScalarTower α M M]
    [IsScalarTower αᵐᵒᵖ M M] [IsCentralScalar α M] (c : Con M) : IsCentralScalar α c.Quotient where
  op_smul_eq_smul a := Quotient.ind' fun m => congr_arg Quotient.mk'' <| op_smul_eq_smul a m

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