smul — Mathlib

English

The product of SMul-regular elements is SMul-regular.

Русский

Произведение SMul-регулярных элементов сохраняет SMul-регулярность.

LaTeX

$$IsSMulRegular M a \rightarrow IsSMulRegular M s \rightarrow IsSMulRegular M (a • s)$$

Lean4

/-- The product of `M`-regular elements is `M`-regular. -/
theorem smul (ra : IsSMulRegular M a) (rs : IsSMulRegular M s) : IsSMulRegular M (a • s) := fun _ _ ab =>
  rs (ra ((smul_assoc _ _ _).symm.trans (ab.trans (smul_assoc _ _ _))))

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