mathlib3

d840349d - feat(algebra/algebra/basic): make algebra_map a low prio has_lift_t (#16567)

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. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>