mathlib3

246853d5 - feat(topology/algebra/module/finite_dimension): `can_lift` instances (#17773)

feat(topology/algebra/module/finite_dimension): `can_lift` instances (#17773) Those instances are quite practical to avoid using `linear_map.to_continuous_linear_map`/`linear_equiv.to_continuous_linear_equiv` explicitly in proofs.