The existing definition is nonsense over semirings; this replaces it with a more plausible one, such that:
```lean
example : ¬ LinearIndependent ℕ Nat.succ := by
  intro h
  have := @h (.single 3 1) (.single 1 2)
  simp [Finsupp.single_eq_single_iff] at this
```
which was previously true without the `¬`.
Some of the nonsense semiring results following the definition must then be ungeneralized to rings.

I've been conservative here and only generalized the ones that generalizer trivially, and are used by important downstream
applications such as `Basis` on semirings. Unimportant downstream applications have instead been ungeneralized to `Ring`.
Many more results can likely be generalized in future.

Some context at https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20.60E.2FL.2FF.60.20and.20.60K.2FL'.2FF.60.20isomorphic.20.3D.3E.20.60.5BE.3AL.5D.3D.5BK.3AL'.5D.60/near/408999160.

The existing definition is nonsense over semirings; this replaces it with a more plausible one, such that:
```lean
example : ¬ LinearIndependent ℕ Nat.succ := by
  intro h
  have := @h (.single 3 1) (.single 1 2)
  simp [Finsupp.single_eq_single_iff] at this
```
which was previously true without the `¬`.
Some of the nonsense semiring results following the definition must then be ungeneralized to rings.

I've been conservative here and only generalized the ones that generalizer trivially, and are used by important downstream
applications such as `Basis` on semirings. Unimportant downstream applications have instead been ungeneralized to `Ring`.
Many more results can likely be generalized in future.

Some context at https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20.60E.2FL.2FF.60.20and.20.60K.2FL'.2FF.60.20isomorphic.20.3D.3E.20.60.5BE.3AL.5D.3D.5BK.3AL'.5D.60/near/408999160.

After the definition is changed in #18426, many results can now be generalized to semirings.

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

A module over a ring is said to be flat if tensoring with it preserves injective linear maps. The same definition remains reasonable over a semiring, because (1) injective linear maps still coincides with monomorphisms over a semiring*; (2) projective modules (in particular, free modules) and localizations are still examples of flat modules over a semiring; (3) we recently fixed the definition of linear independence over semirings (#18426), and flatness of S/R means `(1:S) ⊗[R] ·` preserves linear independence. In fact (2) is the main motivation for this PR: it allows us to unify results about free modules (e.g. polynomial algebras) and localizations over a semiring.

There is a caveat in the definition: injective linear maps need to come from a particular universe, as we can't quantify over all universes. Over a ring, using Baer's criterion and character modules, we may restrict to inclusion maps of (f.g.) ideals, and that was the definition adopted in Mathlib. However, the proof doesn't work over a semiring due to three difficulties: (1) Baer's criterion for injective modules doesn't work over a semiring; (2) Q/Z isn't an injective object in the category of AddCommMonoids, in fact this category [doesn't have enough injectives](https://mathoverflow.net/questions/277284/which-semirings-have-enough-injectives-in-their-category-of-modules); (3) homs into Q/Z does not distinguish points in an AddCommMonoid.

However, we can still show that it suffices to consider injective linear maps between modules in the same universe as the semiring, using the fact that every module is the direct limit of its f.g. submodules, and that taking tensor products commutes with taking direct limits: of course, f.g. modules fit in the same universe as the semiring. We therefore change the definition of flatness to state preservation of injectivity of inclusion of f.g. submodules into f.g. modules in the same universe as the semiring.

As we reorder the lemmas in Flat/Basic.lean, We also change all the iff lemmas to use implicit arguments; several other files need to be fixed for this reason, and as we fix them, we also generalize them to CommSemirings and in some cases golf the proofs.


(*) There are more epimorphisms than surjective homs, e.g. the inclusion of N in Z.