mulLECancellable_mul — Mathlib

English

MulLECancellable (a·b) is equivalent to MulLECancellable a and MulLECancellable b together.

Русский

MulLECancellable (a·b) эквивалентно MulLECancellable a и MulLECancellable b вместе взятые.

LaTeX

$$MulLECancellable (a · b) ↔ (MulLECancellable a) ∧ (MulLECancellable b)$$

Lean4

@[to_additive (attr := simp)]
theorem mulLECancellable_mul [LE α] [CommSemigroup α] [MulLeftMono α] {a b : α} :
    MulLECancellable (a * b) ↔ MulLECancellable a ∧ MulLECancellable b :=
  ⟨fun h ↦ ⟨h.of_mul_left, h.of_mul_right⟩, fun h ↦ h.1.mul h.2⟩

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