of_mul — Mathlib

English

If ab is left-regular, then b is left-regular.

Русский

Если ab леворегулярен, то b также леворегулярен.

LaTeX

$$IsLeftRegular (a * b) → IsLeftRegular b$$

Lean4

/-- If an element `b` becomes left-regular after multiplying it on the left by a left-regular
element, then `b` is left-regular. -/
@[to_additive /-- If an element `b` becomes add-left-regular after adding to it on the left
    an add-left-regular element, then `b` is add-left-regular. -/
    ]
theorem of_mul (ab : IsLeftRegular (a * b)) : IsLeftRegular b :=
  Function.Injective.of_comp (f := (a * ·)) (by rwa [comp_mul_left a b])

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