smul — Mathlib

English

If s is balanced, then for any a in a possibly larger scalar field 𝕝 such that scalars commute with 𝕜, the scaled set a•s is balanced.

Русский

Если множество s сбалансировано, то при любом скалярном множителе a из 𝕝, совместимом со скалярным действием 𝕜, множество a·s сбалансировано.

LaTeX

$$$\forall a\in 𝕝,\, S\text{ Balanced} \implies \text{Balanced}_{\mathfrak{k}}(a\cdot S)$$$$

Lean4

theorem smul (a : 𝕝) (hs : Balanced 𝕜 s) : Balanced 𝕜 (a • s) := fun _b hb =>
  (smul_comm _ _ _).subset.trans <| smul_set_mono <| hs _ hb

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