MathGloss

The French Undergraduate Math corpus comes from here.

Links in the database will take you to the item in the Lean theorem prover as assigned by the curators of the list.

The following is a list of concepts from the France corpus that were not mapped to Wikidata. Our current thoughts as to why they were not mapped is the inclusion of pronouns that refer to missing antecedents and nonstandard plurals. At some point we plan to map these by hand.

  1. Product_of_vector_spaces
  2. Sum_of_subspaces
  3. Generating_sets
  4. Existence_of_bases
  5. Range_of_a_linear_map
  6. Kernel_of_a_linear_map
  7. Algebra_of_endomorphisms_of_a_vector_space
  8. Finite-dimensionality
  9. Isomorphism_with_K^n
  10. Rank_of_a_linear_map
  11. Rank_of_a_set_of_vectors
  12. Isomorphism_with_bidual
  13. Determinant_of_vectors
  14. Determinant_of_endomorphisms
  15. Orientation_of_a_\R-vector_space
  16. Commutative-ring-valued_matrices
  17. Field-valued_matrices
  18. Matrix_representation_of_a_linear_map
  19. Annihilating_polynomials
  20. Generalized_eigenspaces
  21. Subgroup_generated_by_a_subset
  22. Order_of_an_element
  23. Stabilizer_of_a_point
  24. Class_formula
  25. Finite_type_abelian_groups
  26. Complex_roots_of_unity
  27. Primitive_complex_roots_of_unity
  28. Permutation_group_of_a_type
  29. Decomposition_into_transpositions
  30. Decomposition_into_cycles_with_disjoint_support
  31. Orthogonality_of_irreducible_characters
  32. Characters_of_a_finite_dimensional_representation
  33. Subrings
  34. Ring_morphisms
  35. Ring_structure_\Z
  36. Ideal_of_a_commutative_ring
  37. Quotient_rings
  38. Maximal_ideals
  39. Associative_algebra_over_a_commutative_ring
  40. Irreducible_elements
  41. Invertible_elements
  42. Coprime_elements
  43. Unique_factorisation_domain_(UFD)
  44. A[{X_i}]_is_a_UFD_when_A_is_a_UFD
  45. Euclidean_rings
  46. Euclid’s’_algorithm
  47. \Z_is_a_euclidean_ring
  48. Congruence_in_\Z
  49. \Z/n\Z_and_its_invertible_elements
  50. Euler’s_totient_function_(\varphi)
  51. K[X]_is_a_euclidean_ring_when_K_is_a_field
  52. Cyclotomic_polynomials_in_\Q[X]
  53. Polynomial_algebra_in_one_or_several_indeterminates_over_a_commutative_ring
  54. Roots_of_a_polynomial
  55. Relationship_between_the_coefficients_and_the_roots_of_a_split_polynomial
  56. Polynomial_derivative
  57. Decomposition_into_sums_of_homogeneous_polynomials
  58. Subfields
  59. Frobenius_morphisms
  60. Field_\Q_of_rational_numbers
  61. Field_\R_of_real_numbers
  62. Field_\C_of_complex_numbers
  63. \C_is_algebraically_closed
  64. Field_of_fractions_of_an_integral_domain
  65. Algebraic_elements
  66. Transcendental_elements
  67. Algebraic_extensions
  68. Algebraically_closed_fields
  69. Rupture_fields
  70. Splitting_fields
  71. Rational_fraction_fields_with_one_indeterminate_over_a_field
  72. Bilinear_forms
  73. Alternating_bilinear_forms
  74. Symmetric_bilinear_forms
  75. Nondegenerate_forms
  76. Polar_form_of_a_quadratic
  77. Orthogonal_elements
  78. Gram-Schmidt_orthogonalisation
  79. Euclidean_vector_spaces
  80. Hermitian_vector_spaces
  81. Dual_isomorphism_in_the_euclidean_case
  82. Self-adjoint_endomorphism
  83. Diagonalization_of_a_self-adjoint_endomorphism
  84. Decomposition_of_an_orthogonal_transformation_as_a_product_of_reflections
  85. Affine_groups
  86. Convex_subsets
  87. Convex_hull_of_a_subset_of_an_affine_real_space
  88. Isometries_of_a_Euclidean_affine_space
  89. Group_of_isometries_of_a_Euclidean_affine_space
  90. Angles_between_vectors
  91. Cocyclicity
  92. Definition_of_\R
  93. Field_structure
  94. Recurrent_sequences
  95. Limit_infimum_and_supremum
  96. Completeness_of_R
  97. Compact_subsets_of_\R
  98. Connected_subsets_of_\R
  99. Additive_subgroups_of_\R
  100. Convergence_of_p-series_for_p>1
  101. Image_of_a_segment
  102. Continuity_of_monotone_functions
  103. Continuity_of_inverse_functions
  104. Derivative_at_a_point
  105. Derivative_of_a_composition_of_functions
  106. Derivative_of_the_inverse_of_a_function
  107. Higher_order_derivatives_of_functions
  108. C^k_functions
  109. Taylor’s_theorem_with_Lagrange_form_for_remainder
  110. Polynomial_functions
  111. Power_functions
  112. Inverse_hyperbolic_trigonometric_functions
  113. Antiderivative_of_a_continuous_function
  114. Continuity_of_the_limit_of_a_sequence_of_functions
  115. Continuity_of_the_sum_of_a_series_of_functions
  116. Differentiability_of_the_limit_of_a_sequence_of_functions
  117. Differentiability_of_the_sum_of_a_series_of_functions
  118. Weierstrass_polynomial_approximation_theorem
  119. Weierstrass_trigonometric_approximation_theorem
  120. Convex_functions_of_a_real_variable
  121. Characterizations_of_convexity
  122. Convexity_inequalities
  123. Differentiability_with_respect_to_the_complex_variable
  124. Cauchy_formulas
  125. Analyticity_of_a_holomorphic_function
  126. Principle_of_isolated_zeros
  127. Principle_of_analytic_continuation
  128. Holomorphic_stability_under_uniform_convergence
  129. Topology_of_a_metric_space
  130. Finite_product_of_metric_spaces
  131. Limits_of_sequences
  132. Cluster_points
  133. Compactness_in_terms_of_open_covers_(Borel-Lebesgue)
  134. Sequential_compactness_is_equivalent_to_compactness_(Bolzano-Weierstrass)
  135. Complete_metric_spaces
  136. Topology_on_a_normed_vector_space
  137. Banach_open_mapping_theorem
  138. Equivalence_of_norms_in_finite_dimension
  139. Norms_\lVert\cdot\rVert_p_on_\R^n_and_\C^n
  140. Absolutely_convergent_series_in_Banach_spaces
  141. Continuous_linear_maps
  142. Norm_of_a_continuous_linear_map
  143. Uniform_convergence_norm_(sup-norm)
  144. Normed_space_of_bounded_continuous_functions
  145. Its_completeness
  146. Heine-Borel_theorem_(closed_bounded_subsets_are_compact_in_finite_dimension)
  147. Riesz’lemma(unit-ball_characterization_of_finite_dimension)
  148. Orthogonal_projection_onto_closed_vector_subspaces
  149. Inner_product_space_l^2
  150. Its_completeness
  151. Inner_product_space_L^2
  152. Hilbert_bases
  153. Differentiable_functions_on_an_open_subset_of_\R^n
  154. Differentials_(linear_tangent_functions)
  155. K-times_continuously_differentiable_functions
  156. Partial_derivatives_commute
  157. Convexity_of_functions_on_an_open_convex_subset_of_\R^n
  158. Cauchy-Lipschitz_Theorem
  159. Measurable_spaces
  160. Product_of_sigma-algebras
  161. Borel_sigma-algebras
  162. Measurable_functions
  163. Approximation_by_step_functions
  164. Integral_of_positive_measurable_functions
  165. Integrable_functions
  166. Finite_dimensional_vector-valued_integrable_functions
  167. Continuity_of_integrals_with_respect_to_parameters
  168. \mathrm{L}^p_spaces_where_1≤_p≤_∞
  169. Completeness_of_\mathrm{L}^p_spaces
  170. Change_of_variables_for_multiple_integrals
  171. Change_of_variables_to_polar_co-ordinates
  172. Approximation_by_convolution
  173. Regularization_by_convolution
  174. Fourier_series_of_locally_integrable_periodic_real-valued_functions
  175. Independent_sigma-algebra
  176. Borel-Cantelli_lemma_(easy_direction)
  177. Borel-Cantelli_lemma_(difficult_direction)
  178. Discrete_law
  179. Mean_of_a_random_variable
  180. Variance_of_a_real-valued_random_variable
  181. Bernoulli_law
  182. \mathrm{L}^p_convergence
  183. Almost_surely_convergence
  184. Chebychev_inequality
  185. Schwartz_space_of_rapidly_decreasing_functions
  186. Stability_by_derivation
  187. Lagrange_polynomial_of_a_function_at_(n_+_1)_points
  188. Rank_of_a_system_of_linear_equations
  189. Elementary_column_operations
  190. Row-reduced_matrices
  191. Triangularization
  192. Invariant_subspaces_of_an_endomorphism
  193. Kernels_lemma
  194. Jordan-Chevalley-Dunford_decomposition
  195. Endomorphism_exponential
  196. Representations_of_abelian_groups
  197. Dual_groups
  198. Fourier_transform_for_finite_abelian_groups
  199. Class_function_over_a_group
  200. Orthonormal_basis_of_irreducible_characters
  201. Rank_of_a_bilinear_form
  202. Real_classification
  203. Complex_classification
  204. Normal_endomorphism
  205. Diagonalization_of_normal_endomorphisms
  206. Simultaneous_diagonalization_of_two_real_quadratic_forms
  207. Equations_of_affine_subspace
  208. Group_generated_by_homotheties_and_translations
  209. Transformations_fixing_a_basis_of_directions
  210. Isometries_that_preserve_orientation
  211. Direct_and_opposite_similarities_of_the_plane
  212. Classification_of_isometries_in_two_and_three_dimensions
  213. Angles_between_planes
  214. Group_of_isometries_stabilizing_a_subset_of_the_plane_or_of_space
  215. Metric_relations_in_the_triangle
  216. Using_complex_numbers_in_plane_geometry
  217. Quadric_surfaces_in_3-dimensional_Euclidean_affine_spaces
  218. Convergence_of_real_valued-series
  219. Summation_of_comparison_relations
  220. Error_estimation
  221. Products_of_series
  222. Taylor’s_theorem_with_little-o_remainder
  223. Taylor’s_theorem_with_integral_form_for_remainder
  224. Integral_over_a_segment_of_piecewise_continuous_functions
  225. Comparison_test_for_improper_integrals
  226. Power_series_expansion_of_elementary_functions
  227. Representations_of_the
  228. Theorem_of_holomorphic_functions_under_integral_domains
  229. Isolated_singularities
  230. K-th_order_partial_derivatives
  231. Taylor’s_theorem_with_integral_form_for_remainder
  232. Maximal_solutions
  233. Exit_theorem_of_a_compact_subspace
  234. Autonomous_differential_equations
  235. Phase_portraits
  236. Stability_of_equilibrium_points
  237. Linear_differential_systems
  238. Method_of_constant_variation
  239. Duhamel’s_formula
  240. Constant_coefficient_case
This site is open source. Improve this page.