Search results

Rename <code>Rational-Extension-Ring</code> to <code>ℚ-Extension-Ring</code>

elementary-number-theory

improve naming

ring-theory

Status: Open.

#1725 In UniMath/agda-unimath;

· fredrik-bakke opened on Nov 23, 2025

Consider an alternate definition of continuity

analysis

improve naming

metric-spaces

Status: Open.

#1715 In UniMath/agda-unimath;

· lowasser opened on Nov 15, 2025

Naming of reflective global subuniverses

improve naming

orthogonal-factorization-systems

questionFurther information is requestedFurther information is requested

Status: Open.

#1711 In UniMath/agda-unimath;

· fredrik-bakke opened on Nov 14, 2025

Normed vector spaces

linear-algebra

metric-spaces

Status: Open.

#1702 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025

L'Hôpital's Rule

100 theorems

analysis

Status: Open.

#1701 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025

Divergence of the harmonic series

100 theorems

analysis

elementary-number-theory

Status: Open.

#1700 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025

Non-denumerability of the continuum

100 theorems

real-numbers

Status: Open.

#1699 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025

Riemann integration

analysis

Status: Open.

#1698 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025

Irrationality of the square root of 2

100 theorems

elementary-number-theory

real-numbers

Status: Open.

#1697 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025

Ratio test for convergence

analysis

real-numbers

Status: Open.

#1696 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025

Define inner product spaces

linear-algebra

Status: Open.

#1691 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025

Cauchy-Schwarz inequality

100 theorems

formalization-target

linear-algebra

Status: Open.

#1690 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025