Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-13 07:38 e3234f04

View on Github →

feat(algebra/ring): add coercions from →+* to →* and →+ (#1435)

  • feat(algebra/ring): add coercions from →+* to →* and →+
  • two lemmas simplifying casts
  • add squash_cast attributes

Estimated changes