Commit 2024-04-02 15:35 1fb63b46

View on Github →

refactor: golf proof using lmarginal (#10857)

Estimated changes

Modified Mathlib/Data/Matrix/Basis.lean

added theorem Matrix.mulVec_stdBasisMatrix

Modified Mathlib/MeasureTheory/Group/LIntegral.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean