toIsCancelMul — Mathlib

English

If M is a CancelMonoid, then ab = ac implies b = c (cancellation in monoid).

Русский

Если M является CancelMonoid, то ab = ac ⇒ b = c (отмена слева).

LaTeX

$$$\\forall a,b,c \\in M,\\ ab = ac \\Rightarrow b=c$$$

Lean4

/-- Any `CancelMonoid G` satisfies `IsCancelMul G`. -/
@[to_additive /-- Any `AddCancelMonoid G` satisfies `IsCancelAdd G`. -/
    ]
instance (priority := 100) toIsCancelMul (M : Type u) [CancelMonoid M] : IsCancelMul M where

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