mul — Mathlib

English

The product of two left-regular elements is left-regular.

Русский

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

LaTeX

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

Lean4

/-- In a semigroup, the product of left-regular elements is left-regular. -/
@[to_additive /-- In an additive semigroup, the sum of add-left-regular elements is add-left.regular. -/
    ]
theorem mul (lra : IsLeftRegular a) (lrb : IsLeftRegular b) : IsLeftRegular (a * b) :=
  show Function.Injective (((a * b) * ·)) from comp_mul_left a b ▸ lra.comp lrb

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