doc: ensure only a single H1 header per file (leanprover-community#31741)

Author: harahu

Mathlib/Dynamics/Ergodic/Ergodic.lean

@@ -17,7 +17,7 @@ In this file we define ergodic maps / measures together with quasi-ergodic maps
 provide some basic API. Quasi-ergodicity is a weaker condition than ergodicity for which the measure
 preserving condition is relaxed to quasi-measure-preserving.
 
-# Main definitions:
+## Main definitions
 
 * `PreErgodic`: the ergodicity condition without the measure-preserving condition. This exists
   to share code between the `Ergodic` and `QuasiErgodic` definitions.

Mathlib/Order/Filter/CardinalInter.lean

@@ -16,7 +16,7 @@ In this file we define `CardinalInterFilter l c` to be the class of filters with
 property: for any collection of sets `s ∈ l` with cardinality strictly less than `c`,
 their intersection belongs to `l` as well.
 
-# Main results
+## Main results
 * `Filter.cardinalInterFilter_aleph0` establishes that every filter `l` is a
     `CardinalInterFilter l ℵ₀`
 * `CardinalInterFilter.toCountableInterFilter` establishes that every `CardinalInterFilter l c` with

Mathlib/Probability/Independence/BoundedContinuousFunction.lean

@@ -43,19 +43,19 @@ function `f : (Π s : I, E s) → ℝ`, we have `∫ ω in A, f (X · ω) ∂P =
 This again is formulated with different versions. We also provide versions in terms of
 `IndepSets` instead of `Indep`.
 
-# Main statement
+## Main statement
 
 * `indep_comap_process_of_bcf`: A `σ`-algebra `m` is independent from a stochastic process `X`
   if for any `A` such that `MeasurableSet[m] A`, any `I : Finset S`, and any bounded continuous
   function `f : (Π s : I, E s) → ℝ`, we have
   `∫ ω in A, f (X · ω) ∂P = P.real A * ∫ ω, f (X · ω) ∂P`.
 
-# Notations
+## Notations
 
 to avoid writing `boundedContinuousFunction` in the names, which is quite lengthy, we abbreviate it
 to `bcf`.
 
-# Tags
+## Tags
 
 independence, bounded continuous functions
 -/

Mathlib/RingTheory/Localization/AtPrime/Extension.lean

@@ -16,7 +16,7 @@ In this file, we study the relation between the (nonzero) prime ideals of `Sₚ`
 ideals of `S` above `p`. In particular, we prove that (under suitable conditions) they are in
 bijection.
 
-# Main definitions and results
+## Main definitions and results
 
 - `IsLocalization.AtPrime.mem_primesOver_of_isPrime`: The nonzero prime ideals of `Sₚ` are
   primes over the maximal ideal of `Rₚ`.