mul — Mathlib

English

In a semigroup, the product of regular elements is regular.

Русский

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

LaTeX

$$IsRegular a → IsRegular b → IsRegular (a * b)$$

Lean4

/-- In a semigroup, the product of regular elements is regular. -/
@[to_additive /-- In an additive semigroup, the sum of add-regular elements is add-regular. -/
    ]
theorem mul (rra : IsRegular a) (rrb : IsRegular b) : IsRegular (a * b) :=
  ⟨rra.left.mul rrb.left, rra.right.mul rrb.right⟩

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