isRightCancelAdd_iff — Mathlib

English

IsRightCancelAdd on α^{op} is equivalent to IsRightCancelAdd on α.

Русский

IsRightCancelAdd на α^{op} эквивалентен IsRightCancelAdd на α.

LaTeX

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

Lean4

theorem isRightCancelAdd_iff [Add α] : IsRightCancelAdd αᵐᵒᵖ ↔ IsRightCancelAdd α
    where
  mp _ := ⟨fun _ _ _ eq ↦ op_injective <| add_right_cancel (congr_arg op eq)⟩
  mpr _ := inferInstance

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