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.

* polynomial-sequences: (149 commits)
  Aha, here's how to get Lean to stop showing S.elems' in the infoview.
  Try satisfying the linter gods again.
  Probably enough initial tidying to send the PR.
  Kill more temporary names.
  Touch more natDegree.
  Does protected satisfy the docstring linter?
  Bit shorter.
  More
  Quiet linters.
  Remove redundant imports.
  Copyright header and more twiddling.
  Rename lemma to 'degree_smul_of_leadingCoeff_rightRegular' and split out
  feat(Polynomial): polynomial sequences are bases for R[X]
  chore(Dynamics/PeriodicPts): don't import `MonoidWithZero` (#20765)
  chore(Associated): split out `Ring` results (#20737)
  feat(AlgebraicGeometry): flat morphisms of schemes (#19790)
  feat(AlgebraicGeometry): scheme-theoretic fibre (#19427)
  chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785)
  doc: typo (#20829)
  feat(CategoryTheory): condition for an induced functor between comma categories to be final  (#20139)
  feat(1000.yaml): allow statements of theorems also (#20637)
  feat(Algebra/Homology/Embedding): homology of truncGE' (#19570)
  chore: cleanup many porting notes in Combinatorics (#20823)
  chore: eliminate porting notes about `deriving Fintype` (#20820)
  feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808)
  feat: define bases of root pairings (#20667)
  feat(Tactic): basic ConcreteCategory support for elementwise (#20811)
  feat(CategoryTheory): define unbundled `ConcreteCategory` class  (#20810)
  chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809)
  feat: `CommSemiring (NonemptyInterval ℚ≥0)` (#20783)
  chore(yaml_check.py): re-format (#20807)
  feat: elementary estimate for Real.log (#20766)
  feat: definition of linear topologies (#14990)
  feat(RingTheory): flatness over a semiring (#19115)
  feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#19550)
  feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex (#19203)
  feat(Algebra/Ring): `RingEquiv.piUnique` (#20794)
  feat(RingTheory/LocalRing): add instance `Unique (MaximalSpectrum R)` for a local ring `R` (#20801)
  chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802)
  chore: restore `def` to `adicCompletion` (#20796)
  refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643)
  feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544)
  chore(Mathlib/Computability/TuringMachine): split file (#20790)
  feat(Data/Finset/Card): add `InjOn` and `SurjOn` versions of finset cardinality lemmas (#20753)
  feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752)
  feat(Set/Finite): a set is finite if its image and fibers are finite (#20751)
  chore: cleanup .gitignore files (#20795)
  feat(Topology/Group/Profinite):  Profinite group is limit of finite group (#16992)
  feat(Combinatorics/SimpleGraph): vertices in cycles (#20602)
  CI: merge `bot_fix_style` actions (#20789)
  ...