Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-28 12:46 17f83409

View on Github →

chore(data/equiv/basic): simp to_fun to coe (#2256)

  • chore(data/equiv/basic): simp to_fun to coe
  • fix proofs
  • Update src/data/equiv/basic.lean
  • fix proof
  • partially removing to_fun
  • finish switching to coercions

Estimated changes

added theorem equiv.inv_fun_as_coe
added theorem equiv.to_fun_as_coe