analysis icon indicating copy to clipboard operation
analysis copied to clipboard
verified publisher icon math-comp

Put `iavg` in its own file

Open affeldt-aist opened this issue 8 months ago • 1 comments

https://github.com/math-comp/analysis/blob/3cd35520dc1d14ef272e2c6a25f41a94582ab041/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v#L368

affeldt-aist avatar Apr 02 '25 23:04 affeldt-aist

Indirectly related: this merged PR https://github.com/math-comp/analysis/pull/1494 changed the definition of iavg

affeldt-aist avatar Jun 05 '25 02:06 affeldt-aist