mathlib

48ddfd55 - chore(linear_algebra/basic): golf `linear_equiv.smul_of_unit` (#12190)

chore(linear_algebra/basic): golf `linear_equiv.smul_of_unit` (#12190) This already exists more generally as `distrib_mul_action.to_linear_equiv`. The name is probably more discoverable and it needs fewer arguments, so I've left it around for now.