left_cancel — Mathlib

English

If G is a group and P is a G-set with MulAction, then there is an IsLeftCancelSMul G P instance, i.e., left cancellation holds for the action.

Русский

Если G — группа и P — множество с действием, то существует экземпляр IsLeftCancelSMul G P; левое отменение действия действительно.

LaTeX

$$$ [Group\ G] \; [MulAction\ G\ P] \Rightarrow IsLeftCancelSMul\ G\ P$$$

Lean4

@[to_additive]
theorem left_cancel {G P} [SMul G P] [IsCancelSMul G P] (a : G) (b c : P) : a • b = a • c → b = c :=
  IsLeftCancelSMul.left_cancel' a b c

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