instIsLeftCancelSMul_1 — Mathlib

English

For G and P with SMul and IsCancelSMul, the left cancellation law holds: a • b = a • c implies b = c.

Русский

Для G и P с SMul и IsCancelSMul выполняется левое отменяющее свойство: a • b = a • c ⇒ b = c.

LaTeX

$$$ a \cdot b = a \cdot c \Rightarrow b = c $$$

Lean4

@[to_additive]
instance [Group G] [MulAction G P] : IsLeftCancelSMul G P where
  left_cancel' a b c h := by rw [← inv_smul_smul a b, h, inv_smul_smul]

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