of_smul — Mathlib

English

If a is the left-multiplication by an element that is SMul-regular, and a • s is SMul-regular, then s is SMul-regular.

Русский

Если a • s SMul-регулярно и a — SMul-регулярен, тогда s SMul-регулярен.

LaTeX

$$IsSMulRegular M (a) ???$$

Lean4

/-- If an element `b` becomes `M`-regular after multiplying it on the left by an `M`-regular
element, then `b` is `M`-regular. -/
theorem of_smul (a : R) (ab : IsSMulRegular M (a • s)) : IsSMulRegular M s :=
  @Function.Injective.of_comp _ _ _ (fun m : M => a • m) _ fun c d cd =>
    by
    dsimp only [Function.comp_def] at cd
    rw [← smul_assoc, ← smul_assoc] at cd
    exact ab cd

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