mathlib3 documentation

control.equiv_functor.instances

equiv_functor instances #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We derive some equiv_functor instances, to enable equiv_rw to rewrite under these functions.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations