mul — Mathlib

English

If a and b are both cancellable in a compatible ordered monoid, then their product a·b is cancellable.

Русский

Если элементa и элемент b в совместимом упорядоченном полугруппе с сохранением сокращения, их произведение a·b сохраняет свойство сокращения.

LaTeX

$$MulLECancellable a → MulLECancellable b → MulLECancellable (a · b)$$

Lean4

@[to_additive]
theorem mul [Semigroup α] {a b : α} (ha : MulLECancellable a) (hb : MulLECancellable b) : MulLECancellable (a * b) :=
  fun c d hcd ↦ hb <| ha <| by rwa [← mul_assoc, ← mul_assoc]

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