mathlib

13563978 - refactor(linear_algebra/*): linear_equiv.of_bijective over semirings (#9061)

refactor(linear_algebra/*): linear_equiv.of_bijective over semirings (#9061) `linear_equiv.of_injective` and `linear_equiv.of_bijective` took as assumption `f.ker = \bot`, which is equivalent to injectivity of `f` over rings, but not over semirings. This PR changes the assumption to `injective f`. For reasons of symmetry, the surjectivity assumption is also switched to `surjective f`. As a consequence, this PR also renames: * `linear_equiv_of_ker_eq_bot` to `linear_equiv_of_injective` * `linear_equiv_of_ker_eq_bot_apply` to `linear_equiv_of_injective_apply`