instIsRightCancelAdd — Mathlib

English

IsRightCancelAdd on α^{op} holds when α has Add and IsRightCancelAdd.

Русский

Правая отмена сложения сохраняется на α^{op} при наличии IsRightCancelAdd α.

LaTeX

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

Lean4

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

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