* 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)
  ...