Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-11 03:45 d840349d

View on Github →

feat(algebra/algebra/basic): make algebra_map a low prio has_lift_t (#16567) Make algebra_map a coercion (or more precisely a has_lift_t). I have an example where making algebra_map a coercion makes a lot of code far less messy and I'm wondering whether it's a good idea in general.

Estimated changes