Skip to content

[Merged by Bors] - feat: generalize ae_hasDerivAt_integral to Banach spaces#40976

Closed
certik wants to merge 3 commits into
leanprover-community:masterfrom
certik:lebesgue
Closed

[Merged by Bors] - feat: generalize ae_hasDerivAt_integral to Banach spaces#40976
certik wants to merge 3 commits into
leanprover-community:masterfrom
certik:lebesgue

chore: move shared assumptions into a variable line

b459ac2
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Jun 24, 2026 in 1m 12s