isRightCancelMul — Mathlib

English

If Add α and IsRightCancelAdd α hold, then Multiplicative α has right-cancellation: a*b = a'*b implies a=a'.

Русский

Если Add α и IsRightCancelAdd α есть, тогда Multiplicative α имеет правую отмену: a*b = a'*b ⇒ a=a'.

LaTeX

$$Multiplicative isRightCancelMul: ∀ a,b,c, a*b = c*b → a = c$$

Lean4

instance isRightCancelMul [Add α] [IsRightCancelAdd α] : IsRightCancelMul (Multiplicative α) :=
  ⟨fun _ _ _ ↦ add_right_cancel (G := α)⟩

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