Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-26 10:05 ea10e173

View on Github →

feat(data/equiv/functor): bifunctor.map_equiv (#2241)

feat(data/equiv/functor): bifunctor.map_equiv
add documentation, and make the function an explicit argument
Update src/data/equiv/functor.lean

Estimated changes

Modified src/data/equiv/functor.lean

added def bifunctor.map_equiv

added theorem bifunctor.map_equiv_apply

added theorem bifunctor.map_equiv_symm_apply

modified def functor.map_equiv

added theorem functor.map_equiv_apply

added theorem functor.map_equiv_symm_apply

Modified src/ring_theory/free_comm_ring.lean