chore(undergrad.yaml): updates (#4160)

Added a bunch of things to `undergrad.yaml`: generalized eigenspaces, conjugacy classes in a group, the orthogonal complement, continuity of monotone functions and their inverses, inverse hyperbolic trig functions, radius of convergence.  Also changed (hopefully improved) some translations.



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>

docs/undergrad.yaml

@@ -61,7 +61,7 @@ Linear algebra:
     diagonalization: ''
     triangularization: ''
     invariant subspaces of an endomorphism: ''
-    generalized eigenspaces: ''
+    generalized eigenspaces: 'module.End.generalized_eigenspace'
     kernels lemma: ''
     Dunford decomposition: ''
     Jordan normal form: ''
@@ -89,7 +89,7 @@ Group Theory:
     orbit: 'mul_action.orbit'
     quotient space: 'mul_action.orbit_equiv_quotient_stabilizer'
     class formula: ''
-    conjugacy classes: ''
+    conjugacy classes: 'group.conjugates'
   Abelian group:
     cyclic group: 'is_cyclic'
     finite type abelian groups: ''
@@ -214,7 +214,7 @@ Bilinear and Quadratic Forms Over a Vector Space:
     Euclidean vector spaces: 'inner_product_space'
     Hermitian vector spaces:
     dual isomorphism in the euclidean case:
-    orthogonal complement:
+    orthogonal complement: 'submodule.orthogonal'
     Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
     norm: 'inner_product_space.of_core.to_has_norm'
     orthonormal bases:
@@ -238,7 +238,7 @@ Bilinear and Quadratic Forms Over a Vector Space:
     classification of elements of $\mathrm{O}(3, \R)$:
 
 # 5.
-Affine and Euclidian Geometry:
+Affine and Euclidean Geometry:
   General definitions:
     affine space: 'add_torsor'
     affine function: 'affine_map'
@@ -248,31 +248,30 @@ Affine and Euclidian Geometry:
     equations of affine subspace:
     affine groups:
     affine property:
-    homothetic transformation groups:
-    affinity:
+    group generated by homotheties and translations:
+    transformations fixing a basis of directions: # "affinité", no good English translation
   Convexity:
     convex subsets:
     convex hull of a subset of an affine real space:
     extreme point:
   Euclidean affine spaces:
-    isometries of a Euclidian affine subspace:
-    Euclidian affine space isometry group:
-    Euclidean affine space isometries:
+    isometries of a Euclidean affine space:
+    group of isometries of a Euclidean affine space:
     isometries that do and do not preserve orientation:
-    direct and indirect similarities of the plane:
-    isometric classification in two and three dimensions:
-    angles of vectors: 'inner_product_geometry.angle'
-    angles formed by planes:
+    direct and opposite similarities of the plane:
+    classification of isometries in two and three dimensions:
+    angles between vectors: 'inner_product_geometry.angle'
+    angles between planes:
     inscribed angle theorem:
     cocyclicity:
-    group of isometries stabilizing subset of the plane or space:
+    group of isometries stabilizing a subset of the plane or of space:
     regular polygons:
     metric relations in the triangle:
     using complex numbers in plane geometry:
   Application of quadratic forms to study proper conic sections of the affine euclidean plane:
     focus:
     eccentricity:
-    quadratics on 3 dimensional euclidean affine spaces:
+    quadric surfaces in 3-dimensional Euclidean affine spaces:
 
 # 6.
 Single Variable Real Analysis:
@@ -309,13 +308,13 @@ Single Variable Real Analysis:
     limits: 'filter.tendsto'
     intermediate value theorem: 'intermediate_value_Icc'
     image of a segment: 'real.image_Icc'
-    continuity of monotonic functions:
-    continuity of inverse functions:
+    continuity of monotonic functions: 'continuous_of_strict_mono_surjective'
+    continuity of inverse functions: 'homeomorph_of_strict_mono_continuous'
   Differentiability:
     derivative at a point: 'has_deriv_at'
     differentiable functions: 'has_deriv_at'
-    derivative of a composite function: 'deriv.comp'
-    derivative of a reciprocal function: 'has_strict_deriv_at.of_local_left_inverse'
+    derivative of a composition of functions: 'deriv.comp'
+    derivative of the inverse of a function: 'has_strict_deriv_at.of_local_left_inverse'
     Rolle's theorem: 'exists_deriv_eq_zero'
     mean value theorem: 'exists_ratio_deriv_eq_ratio_slope'
     higher order derivatives of functions: 'iterated_deriv'
@@ -332,11 +331,11 @@ Single Variable Real Analysis:
     rational functions:
     logarithms: 'real.log'
     exponential: 'real.exp'
-    power functions: 'monoid.pow'
-    (circular) trigonometric functions: 'real.sin'
+    power functions: 'real.rpow'
+    trigonometric functions: 'real.sin'
     hyperbolic trigonometric functions: 'real.sinh'
-    inverse (circular) trigonometric functions: 'real.arcsin'
-    inverse hyperbolic trigonometric functions:
+    inverse trigonometric functions: 'real.arcsin'
+    inverse hyperbolic trigonometric functions: 'real.arsinh'
   Integration:
     integral over a segment of piecewise continuous functions:
     antiderivatives:
@@ -365,13 +364,13 @@ Single Variable Real Analysis:
 # 7.
 Single Variable Complex Analysis:
   Complex Valued series:
-    radius of convergence:
-    properties of sums of complex valued series on their disks of convergence:
-    continuity:
+    radius of convergence: 'formal_multilinear_series.radius'
+#    properties of sums of complex valued series on their disks of convergence: (this is a heading?)
+    continuity: 'has_fpower_series_on_ball.continuous_on'
     differentiability with respect to the complex variable:
     antiderivative:
-    complex exponentials:
-    extension of circular functions to the complex plane:
+    complex exponential: 'complex.exp'
+    extension of trigonometric functions to the complex plane: 'complex.sin'
     power series expansion of elementary functions:
   Functions on one complex variable:
     holomorphic functions: