Documentation

Mathlib.Deprecated.Equiv

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.

source
@[deprecated]
instance instIsLeftCancelCoeEquivForallForallArrowCongr {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [IsLeftCancel α₁ f] :
IsLeftCancel β₁ ((e.arrowCongr (e.arrowCongr e)) f)
Equations
  • ⋯ = ⋯
source
@[deprecated]
instance instIsRightCancelCoeEquivForallForallArrowCongr {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ ≃ β₁) (f : α₁ → α₁ → α₁) [IsRightCancel α₁ f] :
IsRightCancel β₁ ((e.arrowCongr (e.arrowCongr e)) f)
Equations
  • ⋯ = ⋯