Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
box_integral.integration_params.GP_le
Modification history
2022-09-02 10:49
src/analysis/box_integral/partition/filter.lean
chore(analysis/box_integral): use GP instead of bot (#15939) …
Added
box_integral.integration_params.GP_le
View on Github →