Commit 2024-06-10 10:01 d543653e

View on Github →

chore: fix "unnecessary have" lint errors (#13680)

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/Basic.lean

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

Modified Mathlib/RingTheory/WittVector/WittPolynomial.lean