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 _ _ _))))