instIsLeftCancelAdd — Mathlib

English

IsLeftCancelAdd on α^{op} holds whenever α has Add and IsLeftCancelAdd.

Русский

Левая отмена сложения сохраняется на α^{op} при наличии α с операцией сложения и свойством IsLeftCancelAdd.

LaTeX

$$$\\\\operatorname{IsLeftCancelAdd}(\\\\alpha^{\\\\mathrm{op}}) \\\\iff \\\\operatorname{IsLeftCancelAdd}(\\\\alpha)$$$

Lean4

instance [Add α] [IsLeftCancelAdd α] : IsLeftCancelAdd αᵐᵒᵖ where
  add_left_cancel _ _ _ eq := unop_injective <| add_left_cancel (congr_arg unop eq)

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