instIsCancelSMul — Mathlib

English

If G is CancelMonoid, then IsCancelSMul G G holds with left and right cancellation axioms derived from multiplication.

Русский

Если G — CancelMonoid, тогда IsCancelSMul G G выполняется с левым и правым отменяющими свойствами, получаемыми из умножения.

LaTeX

$$$ [CancelMonoid G] : IsCancelSMul G G$$$

Lean4

@[to_additive]
instance [CancelMonoid G] : IsCancelSMul G G
    where
  left_cancel' := IsLeftCancelMul.mul_left_cancel
  right_cancel' _ _ _ := mul_right_cancel

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