upstream some local properties of modules

Stream: mathlib4

[Yongle Hu]

We are going to upstream some of the local properties of modules project code about local property of Function.Exact, Function.Injective, Module.Flat, NoZeroSMulDivisors, Module.FinitePresentation and so on.

[Johan Commelin]

Thanks, feel free to announce the PRs here. Or create an issue on Github that lists all those PRs. That might help reviewers see the larger picture to which individual PRs belong.

[Yongle Hu]

Opened #19080: prove that Function.Injective, Function.Surjective, Function.Bijective and Function.Exact are local properties.

[Yongle Hu]

Opened #19085: prove that Module.Flat is a local property.