Commit 2023-12-23 18:42 4a335977

View on Github →

chore(Data/Set/Pointwise): golf (#9205)

Estimated changes

Modified Mathlib/Data/Set/Pointwise/Basic.lean

added theorem Set.BddAbove.mul

deleted theorem Set.bddAbove_mul