smul — Mathlib

English

If a is star-normal, then r • a is star-normal for any r.

Русский

Если a звёздно-нормален, то для любого r элемент r • a звёздно-нормален.

LaTeX

$$$\forall r\in R,\; \forall a\in A,\; IsStarNormal(a) \Rightarrow IsStarNormal(r\cdot a)$$$

Lean4

protected instance smul {R A : Type*} [SMul R A] [Star R] [Star A] [Mul A] [StarModule R A] [SMulCommClass R A A]
    [IsScalarTower R A A] (r : R) (a : A) [ha : IsStarNormal a] : IsStarNormal (r • a) where
  star_comm_self := star_smul r a ▸ ha.star_comm_self.smul_left (star r) |>.smul_right r

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