instIsCentralScalar — Mathlib

English

If M acts on X with IsCentralScalar X, then IsCentralScalar M (SeparationQuotient X).

Русский

Если у X есть центральный скаляр, то на SeparationQuotient X есть соответствующий центральный скаляр.

LaTeX

$$IsCentralScalar M (SeparationQuotient X)$$

Lean4

@[to_additive]
instance instIsCentralScalar [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : IsCentralScalar M (SeparationQuotient X) where
  op_smul_eq_smul a := surjective_mk.forall.2 (congr_arg mk <| op_smul_eq_smul a ·)

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