smul — Mathlib

English

If r is homogeneous of some degree, then multiplying by a scalar s preserves the degree: s·r is homogeneous of the same degree.

Русский

Если r гомогенный по степени, то скалярное умножение на s сохраняет ту же степень.

LaTeX

$$If hr : SetLike.IsHomogeneousElem A r, then SetLike.IsHomogeneousElem A (s • r)$$

Lean4

theorem smul [CommSemiring S] [Semiring R] [Algebra S R] {A : ι → Submodule S R} {s : S} {r : R}
    (hr : SetLike.IsHomogeneousElem A r) : SetLike.IsHomogeneousElem A (s • r) :=
  let ⟨i, hi⟩ := hr
  ⟨i, Submodule.smul_mem _ _ hi⟩

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