Skip to content

[Merged by Bors] - feat(MeasureTheory): the integral of a vector-valued function against a vector measure is additive#30230

Closed
CoolRmal wants to merge 30 commits into
leanprover-community:masterfrom
CoolRmal:VectorMeasureIntegral
Closed

[Merged by Bors] - feat(MeasureTheory): the integral of a vector-valued function against a vector measure is additive#30230
CoolRmal wants to merge 30 commits into
leanprover-community:masterfrom
CoolRmal:VectorMeasureIntegral

fix

0606ced
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded May 26, 2026 in 1m 13s