instIsLeftCancelSMul — Mathlib

English

If G is a LeftCancelMonoid, then the action of G on itself yields an IsLeftCancelSMul instance: left_cancel' holds by multiplication cancellation on the left.

Русский

Если G — леводольный моноид, то действие G на G задаёт IsLeftCancelSMul: левое отменение следует из отмены умножения слева.

LaTeX

$$$ [\text{LeftCancelMonoid } G] \Rightarrow IsLeftCancelSMul\ G\ G$$$

Lean4

@[to_additive]
instance [LeftCancelMonoid G] : IsLeftCancelSMul G G where left_cancel' := IsLeftCancelMul.mul_left_cancel

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