doc(overview): pluralization convention (#5583)

Normalized pluralizations, according to the convention @PatrickMassot described

docs/overview.yaml

@@ -9,23 +9,23 @@ General algebra:
     monad: 'category_theory.monad'
     comma category: 'category_theory.comma'
     limits: 'category_theory.limits.is_limit'
-    presheafed spaces: 'algebraic_geometry.PresheafedSpace'
-    sheafed spaces: 'algebraic_geometry.SheafedSpace'
+    presheafed space: 'algebraic_geometry.PresheafedSpace'
+    sheafed space: 'algebraic_geometry.SheafedSpace'
     monoidal category: 'category_theory.monoidal_category'
     cartesian closed: 'category_theory.cartesian_closed'
     abelian category: 'category_theory.abelian'
 
   Numbers:
-    natural numbers: 'nat'
-    integers: 'int'
-    rational numbers: 'rat'
-    continued fractions: 'continued_fraction'
-    real numbers: 'real'
-    extended real numbers: 'ereal'
-    complex numbers: 'complex'
-    "$p$-adic numbers": 'padic'
-    "$p$-adic integers": 'padic_int'
-    hyper-real numbers: 'hyperreal'
+    natural number: 'nat'
+    integer: 'int'
+    rational number: 'rat'
+    continued fraction: 'continued_fraction'
+    real number: 'real'
+    extended real number: 'ereal'
+    complex number: 'complex'
+    "$p$-adic number": 'padic'
+    "$p$-adic integer": 'padic_int'
+    hyper-real number: 'hyperreal'
 
   Group theory:
     group: 'group'
@@ -42,7 +42,7 @@ General algebra:
 
   Rings:
     ring: 'ring'
-    ring morphisms: 'ring_hom'
+    ring morphism: 'ring_hom'
     the category of rings: 'Ring'
     subring: 'is_subring'
     local ring: 'local_ring'
@@ -51,27 +51,27 @@ General algebra:
 
   Ideals and quotients:
     ideal of a commutative ring: 'ideal'
-    quotient rings: 'ideal.quotient'
-    prime ideals: 'ideal.is_prime'
+    quotient ring: 'ideal.quotient'
+    prime ideal: 'ideal.is_prime'
     prime spectrum: 'prime_spectrum'
     Zariski topology: 'prime_spectrum.zariski_topology'
-    maximal ideals: 'ideal.is_maximal'
+    maximal ideal: 'ideal.is_maximal'
     Chinese remainder theorem: 'ideal.quotient_inf_ring_equiv_pi_quotient'
     localization: 'localization'
     fractional ideal: 'ring.fractional_ideal'
 
   Divisibility in integral domains:
-    irreducible elements: 'irreducible'
-    coprime elements: 'is_coprime'
+    irreducible element: 'irreducible'
+    coprime element: 'is_coprime'
     unique factorisation domain: 'unique_factorization_monoid'
     greatest common divisor: 'gcd_monoid.gcd'
     least common multiple: 'gcd_monoid.lcm'
     principal ideal domain: 'submodule.is_principal'
-    Euclidean domains: 'euclidean_domain'
+    Euclidean domain: 'euclidean_domain'
     Euclid's' algorithm: 'nat.xgcd'
     Euler's totient function ($\varphi$): 'nat.totient'
-    sums of two squares: 'nat.prime.sum_two_squares'
-    sums of four squares: 'nat.sum_four_squares'
+    sum of two squares: 'nat.prime.sum_two_squares'
+    sum of four squares: 'nat.sum_four_squares'
     quadratic reciprocity: 'zmod.quadratic_reciprocity'
     Lucas-Lehmer primality test: 'lucas_lehmer_sufficiency'
 
@@ -102,16 +102,16 @@ General algebra:
     Clifford algebra: 'clifford_algebra'
 
   Field theory:
-    fields: 'field'
+    field: 'field'
     characteristic of a ring: 'ring_char'
     characteristic zero: 'char_zero'
     characteristic p: 'char_p'
-    Frobenius morphisms: 'frobenius'
+    Frobenius morphism: 'frobenius'
     algebraically closed field: 'is_alg_closed'
     existence of algebraic closure of a field: 'algebraic_closure'
     $\C$ is algebraically closed: 'complex.exists_root'
     field of fractions of an integral domain: 'fraction_map'
-    algebraic extensions: 'algebra.is_algebraic'
+    algebraic extension: 'algebra.is_algebraic'
     rupture field: 'adjoin_root'
     splitting field: 'polynomial.splitting_field'
     perfect closure: 'perfect_closure'
@@ -130,7 +130,7 @@ Linear algebra:
     quotient space: 'submodule.quotient'
     tensor product: 'tensor_product'
     noetherian module: 'is_noetherian'
-    bases: 'is_basis'
+    basis: 'is_basis'
     multilinear map: 'multilinear_map'
     alternating map: 'alternating_map'
     general linear group: 'linear_map.general_linear_group'
@@ -154,16 +154,14 @@ Linear algebra:
     eigenvalue: 'module.End.has_eigenvalue'
     eigenvector: 'module.End.has_eigenvector'
     existence of an eigenvalue: 'module.End.exists_eigenvalue'
-
-
   Bilinear and quadratic forms:
-    bilinear forms: 'bilin_form'
-    alternating bilinear forms: 'alt_bilin_form.is_alt'
-    symmetric bilinear forms: 'sym_bilin_form.is_sym'
+    bilinear form: 'bilin_form'
+    alternating bilinear form: 'alt_bilin_form.is_alt'
+    symmetric bilinear form: 'sym_bilin_form.is_sym'
     matrix representation: 'bilin_form.to_matrix'
     quadratic form: 'quadratic_form'
     polar form of a quadratic: 'quadratic_form.polar'
-    Euclidean vector spaces: 'inner_product_space'
+    Euclidean vector space: 'inner_product_space'
     Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
     self-adjoint endomorphism: 'bilin_form.is_self_adjoint'
 
@@ -190,10 +188,10 @@ Topology:
     topological fiber bundle: 'is_topological_fiber_bundle'
   Uniform notions:
     uniform space: 'uniform_space'
-    uniformly continuous functions: 'metric.uniform_continuous_iff'
+    uniformly continuous function: 'metric.uniform_continuous_iff'
     uniform convergence: 'tendsto_uniformly'
-    Cauchy filters: 'cauchy'
-    Cauchy sequences: 'cauchy_seq'
+    Cauchy filter: 'cauchy'
+    Cauchy sequence: 'cauchy_seq'
     completeness: 'complete_space'
     completion: 'completion'
     Heine-Cantor theorem: 'compact_space.uniform_continuous_of_continuous'
@@ -214,7 +212,7 @@ Topology:
     ball: 'metric.ball'
     sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'metric.compact_iff_seq_compact'
     Heine-Borel theorem (proper metric space version): 'metric.compact_iff_closed_bounded'
-    Lipschitz functions: 'lipschitz_with'
+    Lipschitz function: 'lipschitz_with'
     contraction mapping theorem: 'contracting_with.exists_fixed_point'
     Baire theorem: 'dense_Inter_of_open'
     Arzela-Ascoli theorem: 'bounded_continuous_function.arzela_ascoli'
@@ -228,7 +226,7 @@ Analysis:
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'
     finite dimensional normed spaces over complete normed fields are complete: 'submodule.complete_of_finite_dimensional'
     Heine-Borel theorem (finite dimensional normed spaces are proper): 'finite_dimensional.proper'
-    continuous linear maps: 'continuous_linear_map'
+    continuous linear map: 'continuous_linear_map'
     norm of a continuous linear map: 'linear_map.mk_continuous'
     Banach open mapping theorem: 'open_mapping'
     absolutely convergent series in Banach spaces: 'summable_of_summable_norm'
@@ -239,46 +237,46 @@ Analysis:
     completeness of spaces of bounded continuous functions: 'bounded_continuous_function.complete_space'
 
   Differentiability:
-    differentiable functions between normed vector spaces: 'has_fderiv_at'
+    differentiable function between normed vector spaces: 'has_fderiv_at'
     derivative of a composition of functions: 'has_fderiv_at.comp'
     derivative of the inverse of a function: 'has_fderiv_at.of_local_left_inverse'
     Rolle's theorem: 'exists_deriv_eq_zero'
     mean value theorem: 'exists_ratio_deriv_eq_ratio_slope'
-    $C^k$ functions: 'times_cont_diff'
+    $C^k$ function: 'times_cont_diff'
     Leibniz formula: 'fderiv_mul'
     local extrema: 'is_local_min.fderiv_eq_zero'
     inverse function theorem: 'has_strict_fderiv_at.to_local_inverse'
     implicit function theorem: 'implicit_function_data.implicit_function'
     analytic function: 'analytic_at'
 
   Convexity:
-    convex functions: 'convex_on'
+    convex function: 'convex_on'
     characterization of convexity: 'convex_on_of_deriv2_nonneg'
     Jensen's inequality (finite sum version): 'convex_on.map_sum_le'
     Jensen's inequality (integral version): 'convex_on.map_integral_le'
     convexity inequalities: 'analysis/mean_inequalities.html'
     Carathéodory's theorem: 'convex_hull_eq_union'
 
   Special functions:
-    logarithms: 'real.log'
+    logarithm: 'real.log'
     exponential: 'real.exp'
     trigonometric functions: 'real.sin'
     inverse trigonometric functions: 'real.arcsin'
     hyperbolic trigonometric functions: 'real.sinh'
     inverse hyperbolic trigonometric functions: 'real.arsinh'
 
   Measures and integral calculus:
-    sigma-algebras: 'measurable_space'
-    measurable functions: 'measurable'
-    the category of measurable space: 'Meas'
-    Borel sigma-algebras: 'borel_space'
+    sigma-algebra: 'measurable_space'
+    measurable function: 'measurable'
+    the category of measurable spaces: 'Meas'
+    Borel sigma-algebra: 'borel_space'
     positive measure: 'measure_theory.measure'
     Lebesgue measure: 'measure_theory.real.measure_space'
     Giry monad: 'measure_theory.measure.measurable_space'
     integral of positive measurable functions: 'measure_theory.lintegral'
     monotone convergence theorem: 'measure_theory.lintegral_infi_ae'
     Fatou's lemma: 'measure_theory.lintegral_liminf_le'
-    vector-valued integrable functions (Bochner integral): 'measure_theory.integrable'
+    vector-valued integrable function (Bochner integral): 'measure_theory.integrable'
     $L^1$ space: 'measure_theory.l1'
     Bochner integral: 'measure_theory.integral'
     dominated convergence theorem: 'measure_theory.tendsto_integral_of_dominated_convergence'
@@ -287,13 +285,13 @@ Analysis:
 
 Geometry:
   Affine and Euclidean geometry:
-    affine spaces: 'add_torsor'
-    affine functions: 'affine_map'
-    affine subspaces: 'affine_subspace'
-    barycenters: 'finset.affine_combination'
-    affine spans: 'span_points'
+    affine space: 'add_torsor'
+    affine function: 'affine_map'
+    affine subspace: 'affine_subspace'
+    barycenter: 'finset.affine_combination'
+    affine span: 'span_points'
     Euclidean affine space: 'normed_add_torsor'
-    angles of vectors: ' inner_product_geometry.angle'
+    angle: ' inner_product_geometry.angle'
 
   Differentiable manifolds:
     smooth manifold (with boundary and corners): 'smooth_manifold_with_corners'