mathlib3

feat(ring_theory/local_properties): Being (in/sur/bi)jective is local (for linear maps).

#17472

Open