Skip to content

feat(MeasureTheory): coercion of a finite sum of scalar multiples in Lp#40827

Open
FrankieNC wants to merge 4 commits into
leanprover-community:masterfrom
FrankieNC:coefn-sum-smul
Open

feat(MeasureTheory): coercion of a finite sum of scalar multiples in Lp#40827
FrankieNC wants to merge 4 commits into
leanprover-community:masterfrom
FrankieNC:coefn-sum-smul

Commits

Commits on Jun 20, 2026