toAddCancelCommMonoid — Mathlib

English

A canonically ordered additive commutative monoid with ordered subtraction and order-reflecting addition is cancellative.

Русский

Канонически упорядоченная аддитивная коммутативная однородная моноида с упорядоченным вычитанием и отражающим порядком сложением является отменяемой.

LaTeX

$$$$ \forall x,y,z:\ x+z = y+z \Rightarrow x = y $$$$

Lean4

/-- A `CanonicallyOrderedAddCommMonoid` with ordered subtraction and order-reflecting addition is
cancellative. This is not an instance as it would form a typeclass loop.

See note [reducible non-instances]. -/
abbrev toAddCancelCommMonoid : AddCancelCommMonoid α :=
  { (by infer_instance : AddCommMonoid α) with
    add_left_cancel := fun a b c h => by simpa only [add_tsub_cancel_left] using congr_arg (fun x => x - a) h }

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