Sitelet
https://github.com/math-comp/analysis/commits/master/
Skip to content
Navigation Menu
Sign in
Appearance settings
Platform
AI CODE CREATION
GitHub Copilot
Write better code with AI
GitHub Copilot app
Direct agents from issue to merge
MCP Registry
Integrate external tools
DEVELOPER WORKFLOWS
Actions
Automate any workflow
Codespaces
Instant dev environments
Issues
Plan and track work
Code Review
Manage code changes
Code Quality
Enforce quality at merge
APPLICATION SECURITY
GitHub Advanced Security
Find and fix vulnerabilities
Code security
Secure your code as you build
Secret protection
Stop leaks before they start
EXPLORE
Why GitHub
Documentation
Blog
Changelog
Marketplace
View all features
Solutions
BY COMPANY SIZE
Enterprises
Small and medium teams
Startups
Nonprofits
BY USE CASE
App Modernization
DevSecOps
DevOps
CI/CD
View all use cases
BY INDUSTRY
Healthcare
Financial services
Manufacturing
Government
View all industries
View all solutions
Resources
EXPLORE BY TOPIC
AI
Software Development
DevOps
Security
View all topics
EXPLORE BY TYPE
Customer stories
Events & webinars
Ebooks & reports
Business insights
GitHub Skills
SUPPORT & SERVICES
Documentation
Customer support
Community forum
Trust center
Partners
View all resources
Open Source
COMMUNITY
GitHub Sponsors
Fund open source developers
PROGRAMS
Security Lab
Maintainer Community
GitHub Stars
Archive Program
REPOSITORIES
Topics
Trending
Collections
Enterprise
ENTERPRISE SOLUTIONS
Enterprise platform
AI-powered developer platform
AVAILABLE ADD-ONS
GitHub Advanced Security
Enterprise-grade security features
Copilot for Business
Enterprise-grade AI features
Premium Support
Enterprise-grade 24/7 support
Pricing
Search
/
Sign in
Sign up
Appearance settings
You signed in with another tab or window.
Reload
to refresh your session.
You signed out in another tab or window.
Reload
to refresh your session.
You switched accounts on another tab or window.
Reload
to refresh your session.
Dismiss alert
{{ message }}
math-comp
/
analysis
Public
Notifications
You must be signed in to change notification settings
Fork
75
Star
246
Code
Issues
102
Pull requests
77
Actions
Projects
Wiki
Security and quality
0
Insights
Additional navigation options
Code
Issues
Pull requests
Actions
Projects
Wiki
Security and quality
Insights
Commits
Branch selector
master
User selector
All users
Datepicker
All time
Commit history
Commits on Oct 2, 2026
Adapt to https://github.com/rocq-prover/rocq/pull/22548 (#2117)
proux01
authored
9c9f64f
View commit details
Copy full SHA for 9c9f64f
Browse repository at this point
Commits on Oct 1, 2026
Add function to restrict a real to the intervale [min , max] (#2106)
Show description for 013decd
lyonel2017
and
affeldt-aist
authored
013decd
View commit details
Copy full SHA for 013decd
Browse repository at this point
Normedtype 20260924 (#2112)
Show description for 3ba1bf5
affeldt-aist
authored
3ba1bf5
View commit details
Copy full SHA for 3ba1bf5
Browse repository at this point
new series convergence criteria (#2035)
Show description for 6e7bdac
nmolinamounier
authored
6e7bdac
View commit details
Copy full SHA for 6e7bdac
Browse repository at this point
Commits on Sep 30, 2026
unif cont -> cont (#2113)
Show description for afa83b4
affeldt-aist
and
t6s
authored
afa83b4
View commit details
Copy full SHA for afa83b4
Browse repository at this point
Commits on Sep 29, 2026
Add generic facts about einfs and limn_einf (#2107)
Show description for 0be52f3
lyonel2017
and
affeldt-aist
authored
0be52f3
View commit details
Copy full SHA for 0be52f3
Browse repository at this point
Commits on Sep 28, 2026
Compile with +level-tolerance (#2108)
Show description for 86b80ee
proux01
authored
86b80ee
View commit details
Copy full SHA for 86b80ee
Browse repository at this point
Fix packager (#2114)
Show description for dfc3474
proux01
authored
dfc3474
View commit details
Copy full SHA for dfc3474
Browse repository at this point
Commits on Sep 25, 2026
Cleanup old COQ variables in Makefiles (#2111)
Show description for 374700f
proux01
authored
374700f
View commit details
Copy full SHA for 374700f
Browse repository at this point
[CI] Update Nix toolbox (#2110)
proux01
authored
7530e55
View commit details
Copy full SHA for 7530e55
Browse repository at this point
Cleanup old coq commands (#2109)
Show description for db81f92
proux01
authored
db81f92
View commit details
Copy full SHA for db81f92
Browse repository at this point
Commits on Sep 22, 2026
[CI] Add infotheo for Rocq 9.2 (#2105)
proux01
authored
fd300fa
View commit details
Copy full SHA for fd300fa
Browse repository at this point
Commits on Sep 16, 2026
Doc: :memo: Bump up the rocqnavi version (#2102)
yoshihiro503
authored
a0582da
View commit details
Copy full SHA for a0582da
Browse repository at this point
Commits on Sep 11, 2026
Fix opam file for reals-stdlib package (#2101)
proux01
authored
921d430
View commit details
Copy full SHA for 921d430
Browse repository at this point
Commits on Sep 2, 2026
changelog for version 1.18.0 (#2099)
Show description for 00a80bd
affeldt-aist
authored
00a80bd
View commit details
Copy full SHA for 00a80bd
Browse repository at this point
Fix 2050 (#2098)
Show description for dc7afb9
affeldt-aist
authored
dc7afb9
View commit details
Copy full SHA for dc7afb9
Browse repository at this point
Commits on Sep 1, 2026
mv contents of file prodnormedzmodule (#2097)
affeldt-aist
authored
99cd334
View commit details
Copy full SHA for 99cd334
Browse repository at this point
Commits on Aug 31, 2026
fix #1972 (#2095)
Show description for 595e5d0
affeldt-aist
and
IshiguroYoshihiro
authored
595e5d0
View commit details
Copy full SHA for 595e5d0
Browse repository at this point
Commits on Aug 30, 2026
doc summable (#2096)
affeldt-aist
authored
949d0c9
View commit details
Copy full SHA for 949d0c9
Browse repository at this point
fix #1967 (#2088)
affeldt-aist
authored
2e85ddc
View commit details
Copy full SHA for 2e85ddc
Browse repository at this point
Commits on Aug 27, 2026
is_derive_trmx (#2060)
Show description for 73c7aa2
3 people
authored
73c7aa2
View commit details
Copy full SHA for 73c7aa2
Browse repository at this point
measurable bigmax (#2092)
affeldt-aist
authored
45cff6a
View commit details
Copy full SHA for 45cff6a
Browse repository at this point
Commits on Aug 22, 2026
minor gen and rm dup (#2090)
affeldt-aist
authored
e53f4d1
View commit details
Copy full SHA for e53f4d1
Browse repository at this point
add elementary functions to doc (#2089)
affeldt-aist
authored
341063f
View commit details
Copy full SHA for 341063f
Browse repository at this point
Commits on Aug 20, 2026
Adapt to https://github.com/math-comp/math-comp/pull/1622 (#2085)
proux01
authored
fcd4ec5
View commit details
Copy full SHA for fcd4ec5
Browse repository at this point
[CI] Update Nix toolbox (#2087)
proux01
authored
333d22a
View commit details
Copy full SHA for 333d22a
Browse repository at this point
Commits on Aug 18, 2026
add compatibility lemmas for Stdlib `Rcos` and `Rsin` (#2083)
Show description for 7f7f74e
t6s
authored
7f7f74e
View commit details
Copy full SHA for 7f7f74e
Browse repository at this point
Commits on Aug 16, 2026
new `derive.v` lemmas (#2026)
Show description for f694551
nmolinamounier
authored
f694551
View commit details
Copy full SHA for f694551
Browse repository at this point
generalize continuous_comp_cvg (#2082)
Show description for c016f6e
t6s
and
affeldt-aist
authored
c016f6e
View commit details
Copy full SHA for c016f6e
Browse repository at this point
Commits on Aug 15, 2026
fix #2080 (#2081)
affeldt-aist
authored
478f724
View commit details
Copy full SHA for 478f724
Browse repository at this point
Commits on Aug 14, 2026
split trigo.v (#2079)
Show description for dd2fa21
affeldt-aist
authored
dd2fa21
View commit details
Copy full SHA for dd2fa21
Browse repository at this point
chore: :book: Code blocks in Documentation comments (#2077)
yoshihiro503
authored
f9ba3b7
View commit details
Copy full SHA for f9ba3b7
Browse repository at this point
Commits on Aug 12, 2026
mv mathcomp_{extra,compat} (#2075)
affeldt-aist
authored
a362cf0
View commit details
Copy full SHA for a362cf0
Browse repository at this point
chore: :book: Use deflist for Rocqnavi Document (#2078)
yoshihiro503
authored
5454962
View commit details
Copy full SHA for 5454962
Browse repository at this point
Commits on Aug 11, 2026
Gaussian-Gaussian conjugate prior (#43) (#2073)
Show description for d35a7ab
affeldt-aist
and
gbdrt
authored
d35a7ab
View commit details
Copy full SHA for d35a7ab
Browse repository at this point
Previous
Next
You can’t perform that action at this time.