isCentralScalar — Mathlib

English

If the scalar action of R on V2 is central (via the opposite ring), then it is central on the affine map space as well: IsCentralScalar R (AffineMap_k(P1,V2)).

Русский

Если действие R на V2 центрально (через противоположное кольцо), то оно центрально и на пространстве аффинных отображений: IsCentralScalar R (AffineMap_k(P1,V2)).

LaTeX

$$$\forall r\in R,\ m\in (P_1 \to^{\mathrm{aff}}_k V_2),\ r\cdot m = m\cdot r$$$

Lean4

instance isCentralScalar [DistribMulAction Rᵐᵒᵖ V2] [IsCentralScalar R V2] : IsCentralScalar R (P1 →ᵃ[k] V2) where
  op_smul_eq_smul _r _x := ext fun _ => op_smul_eq_smul _ _

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