mul — Mathlib

English

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

Русский

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

LaTeX

$$IsRightRegular a → IsRightRegular b → IsRightRegular (a * b)$$

Lean4

/-- In a semigroup, the product of right-regular elements is right-regular. -/
@[to_additive /-- In an additive semigroup, the sum of add-right-regular elements is add-right-regular. -/
    ]
theorem mul (rra : IsRightRegular a) (rrb : IsRightRegular b) : IsRightRegular (a * b) :=
  show Function.Injective (· * (a * b)) from comp_mul_right b a ▸ rrb.comp rra

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