- D1927: Standard real cosine function
- D5860: Complex matrix eigenmatrix
- R5232: Finite sum of independent gaussian random real numbers is a gaussian random real number
- D1301: Generated subgroup
- R347: Isotonicity of map image
- D1382: Complex euclidean length function
- D326: Cartesian product
- R4913: Strong derivative for euclidean real quadratic form without translation
- D2726: Finite graph
- D4105: Standard counting measure