Note about deprecated files #
This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.
Unbundled algebra classes and Equiv #
This file contains a few deprecated results on the Is* classes introduced in
Mathlib/Deprecated/AlgebraClasses.lean that involve the Equiv type.
@[deprecated]
instance
instIsLeftCancelCoeEquivForallForallArrowCongr
{α₁ : Type u_1}
{β₁ : Type u_2}
(e : α₁ ≃ β₁)
(f : α₁ → α₁ → α₁)
[IsLeftCancel α₁ f]
:
IsLeftCancel β₁ ((e.arrowCongr (e.arrowCongr e)) f)
@[deprecated]
instance
instIsRightCancelCoeEquivForallForallArrowCongr
{α₁ : Type u_1}
{β₁ : Type u_2}
(e : α₁ ≃ β₁)
(f : α₁ → α₁ → α₁)
[IsRightCancel α₁ f]
:
IsRightCancel β₁ ((e.arrowCongr (e.arrowCongr e)) f)