Movatterモバイル変換

UniMath/agda-unimathPublic

NotificationsYou must be signed in to change notification settings
Fork91
Star278

New pull requestNew

78 Open 1,417 Closed

Author

Label

Projects

Milestones

Reviews

Filter by reviews

No reviews Review required Approved review Changes requested

Assignee

Sort

The Cauchy-Schwarz inequality in complex inner product spaces 100 theorems complex-numbers formalization-target linear-algebra

#1754 openedDec 17, 2025 bylowasser • Draft

The reals and complex numbers are locally small complex-numbers foundation real-numbers

#1753 openedDec 16, 2025 bylowasser

Loading…

Standardize an "is zero" predicate on the real numbers real-numbers refactoring

#1752 openedDec 16, 2025 bylowasser

Loading…

Dense subsets of the real numbers metric-spaces real-numbers

#1750 openedDec 11, 2025 bylowasser

Loading…

Smallness of the monomorphism predicate foundation improve naming refactoring

#1749 openedDec 8, 2025 byfredrik-bakke

Loading…

Sine and cosine analysis real-numbers

#1748 openedDec 6, 2025 bylowasser • Draft

The natural exponential function on real numbers analysis real-numbers

#1747 openedDec 6, 2025 bylowasser • Draft

Forks foundation

#1746 openedDec 4, 2025 byfredrik-bakke

Loading…

Define arithmetic and geometric means real-numbers

#1745 openedDec 4, 2025 bylowasser • Draft

Rational powers of positive real numbers real-numbers

#1743 openedDec 3, 2025 bylowasser • Draft

Metric extensions metric-spaces

#1742 openedDec 2, 2025 bymalarbol • Draft

Nonzero natural roots of nonnegative real numbers

#1740 openedDec 2, 2025 bylowasser • Draft

Odd roots of real numbers real-numbers

#1739 openedDec 2, 2025 bylowasser • Draft

Refactor function actions on cauchy approximations metric-spaces

#1738 openedDec 1, 2025 bymalarbol

Loading…

Odd powers of real numbers are strictly increasing real-numbers

#1737 openedNov 30, 2025 bylowasser

Loading…

Equivalences of cospan diagrams foundation

#1736 openedNov 28, 2025 byfredrik-bakke • Draft

Operations on cospans foundation synthetic-homotopy-theory

#1735 openedNov 28, 2025 byfredrik-bakke

Loading…

WIP: Retract of quasicoherently idempotent maps foundation

#1734 openedNov 28, 2025 byfredrik-bakke • Draft

Descent for surjective maps foundation

#1732 openedNov 27, 2025 byfredrik-bakke • Draft

Cleanup of descent properties foundation refactoring synthetic-homotopy-theory

#1730 openedNov 27, 2025 byfredrik-bakke

Loading…

Cauchy metric extensions of pseudometric spaces metric-spaces

#1729 openedNov 26, 2025 bymalarbol • Draft

Decidable retracts foundation

#1728 openedNov 26, 2025 byfredrik-bakke • Draft

Initial metric extensions of pseudometric spaces metric-spaces

#1726 openedNov 23, 2025 bymalarbol • Draft

Some constructions on polynomial endofunctors foundation trees

#1723 openedNov 20, 2025 byfredrik-bakke

Loading…

Equivalences of polynomial endofunctors trees

#1722 openedNov 20, 2025 byfredrik-bakke

Loading…

ProTip! Follow long discussions withcomments:>50.

Movatterモバイル変換

Navigation Menu

Search code, repositories, users, issues, pull requests...

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Movatterモバイル変換

Pull requests: UniMath/agda-unimath

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Pull requests list