mathlib

6d584f17 - refactor(linear_algebra/basic): use `bijective` in `linear_equiv.of_bijective` (#17897)

refactor(linear_algebra/basic): use `bijective` in `linear_equiv.of_bijective` (#17897) The two-argument version is a remnant of when we used to express these in terms of `range` and `ker`, which we dropped due to wanting to support semirings. We already have `equiv.of_bijective`, `ring_equiv.of_bijective`, etc which take a single `function.bijective` argument instead of two arguments; this makes the `linear_equiv` and `lie_equiv` spellings consistent.