toCancelMonoid — Mathlib

English

The CancelMonoid structure on a Group G satisfies the cancellation laws.

Русский

Структура CancelMonoid на группе G удовлетворяет законам отмены.

LaTeX

$$$\\text{CancelMonoid}(G) \\land \\text{cancellation\_laws}(G)$$$

Lean4

@[to_additive]
instance (priority := 100) toCancelMonoid : CancelMonoid G
    where
  mul_right_cancel := fun a b c h ↦ by rw [← mul_inv_cancel_right b a, show b * a = c * a from h, mul_inv_cancel_right]
  mul_left_cancel := fun a {b c} h ↦ by rw [← inv_mul_cancel_left a b, show a * b = a * c from h, inv_mul_cancel_left]

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